proposition: Lemma g2h_eqE (a b: T2) : g2h a = g2h b <-> a = b.
proof: Proof. split . - rewrite -(h2g_g2hK a) -(h2g_g2hK b) !g2h_h2gK => // -> //. - by move => -> . Qed.
imports: mathcomp(all_ssreflect zify) Coq(Logic.Eqdep_dec) hydras(DecPreOrder ON_Generic T2 Gamma0)