equational reasoning for Congruence.Heterogeneous
Groth: rewrote proofs with HetReasoning