agda-stdlib has facilities for doing equational reasoning for various specific library defined relations (example). It also has a type that identifies equality relations defined here. What is the easiest way for me to get access to the same facilities for equational reason I get with propositional equality.
The kit is defined in Relation.Binary.Reasoning.Setoid.
You only need to define a proof S that your relation defines a Setoid and then you can open import Relation.Binary.Reasoning.Setoid S to get the equational reasoning combinators.