proposition: Lemma T1is_succ_ref (a:Epsilon0.T1.T1): T1.T1is_succ a = T1is_succ (h2g a).
proof: Proof. elim: a => /= //. move => a IHa n b /= -> ; case: a IHa => //. Qed.
imports: mathcomp(all_ssreflect zify) Coq(Logic.Eqdep_dec) hydras(DecPreOrder ON_Generic T1 E0)