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