proposition: Lemma T1limit_ref (a:Epsilon0.T1.T1) : T1.T1limit a = T1limit (h2g a).
proof: Proof. elim: a => /= //. move => a IHa n b IHb; cbn; rewrite IHb. move: IHa; case:a => //. move => a n0 b0 IH; cbn; move: IHb; case: b => //. Qed.
imports: mathcomp(all_ssreflect zify) Coq(Logic.Eqdep_dec) hydras(DecPreOrder ON_Generic T1 E0)