proposition: Lemma E0_eqE (x y: E0) : x = y <-> (E0_g2h x = E0_g2h y).
proof: Proof. split. move => Heq; by subst. move => H; by rewrite -(E0_h2g_g2hK x) -(E0_h2g_g2hK y) H. Qed.
imports: mathcomp(all_ssreflect zify) Coq(Logic.Eqdep_dec) hydras(DecPreOrder ON_Generic T1 E0)