proposition: Lemma refines2_R f f' : refines2 f f' <-> forall y z: T1, f (g2h y) (g2h z) = g2h (f' y z).
proof: Proof. split => [Href y z | H x y]. by rewrite -{2}(h2g_g2hK y) -{2}(h2g_g2hK z) ?Href ?g2h_h2gK. by rewrite -{2}(g2h_h2gK x) -{2}(g2h_h2gK y) H h2g_g2hK. Qed.
imports: mathcomp(all_ssreflect zify) Coq(Logic.Eqdep_dec) hydras(DecPreOrder ON_Generic T1 E0)