proposition: Lemma limitb_ref (a:t): limitb a -> T1limit (refine a).
proof: Proof. induction a as [| a l]; cbn. - trivial. - destruct a as [n n0]. destruct n. + discriminate. + simpl T1limit; destruct l. * trivial. * intro H; rewrite IHl; case (refine (p::l)); auto. Qed.
imports: hydras(T1 E0 Comparable) Coq(Arith Logic.Eqdep_dec Peano_dec List Bool Recdef Lia Wellfounded.Inverse_Image Wellfounded.Inclusion RelationClasses )