fact: Fixpoint h2g (alpha : hT2) : T2 := match alpha with hzero => zero | hcons a b n c => cons (h2g a) (h2g b) n (h2g c) end.
imports: mathcomp(all_ssreflect zify) Coq(Logic.Eqdep_dec) hydras(DecPreOrder ON_Generic T2 Gamma0)