proposition: Lemma h2g_diffE (a b : hT1) : h2g a <> h2g b <-> a <> b.
proof: Proof. split => H Heq; [subst; by apply: H | by apply H, h2g_eqE]. Qed.
imports: mathcomp(all_ssreflect zify) Coq(Logic.Eqdep_dec) hydras(DecPreOrder ON_Generic T1 E0)