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