proposition: Lemma LT_path_toS (alpha beta : T1) : beta t1< alpha -> {s : list nat | path_toS beta s alpha}.
proof: Proof. Proof with eauto with T1. transfinite_induction alpha; clear alpha; intros alpha IHalpha H. assert (H0: nf beta) ... assert (H1: nf alpha) ... destruct (zero_limit_succ_dec H1 ) as [[Hzero | Hlimit] | Hsucc]. - subst alpha; destruct (not_LT_zero H). - destruct (canonS_limit_strong H1 Hlimit H) as [j Hj]. destruct (IHalpha (canon alpha (S j))) as [x p]; auto. apply canonS_LT; auto. apply T1limit_not_zero;auto. exists (j::x); eright. { split. intro; subst. - inversion Hlimit. - reflexivity. } assumption. - destruct Hsucc as [gamma [H3 H2]]. subst alpha; destruct (LT_succ_LT_eq_dec H0 H3 H). + destruct (IHalpha gamma) as [x p]; auto. apply LT_succ; auto. exists (0::x); right with gamma; auto. split. * apply succ_not_zero. * now rewrite canon_succ. + subst beta; exists (0::nil); left. * split. -- apply succ_not_zero. -- now rewrite canon_succ. Defined.
imports: hydras(DecPreOrder Canon MoreLists First_toggle OrdNotations) Coq(Lia)