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