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