proposition: Lemma standard_path_lt2 : forall i alpha j beta, (0 < i)%nat -> zero t1< alpha -> standard_path_to j beta i alpha -> beta t1< alpha.
proof: Proof. induction 3. - destruct i. + inversion H. + subst beta; apply canonS_LT. * inversion H0; tauto. * red ; intro; subst; inversion H0. destruct H3; inversion H3. - destruct (T1_eq_dec beta zero). + subst; auto. + destruct (T1_eq_dec (canon alpha i) zero). * rewrite e in H1; assert (beta = zero). { eapply standard_path_zero ; eauto. } subst;auto. * apply LT_trans with (canon alpha i) ; auto. apply IHstandard_path_to; auto with arith. apply not_zero_lt. { destruct i. - simpl; auto with T1. apply nf_canon; eauto with T1. - apply nf_canon, (LT_nf_r H0); auto. } { destruct i; auto. } destruct i. { apply canon0_LT; eauto with T1. intro; subst; auto. } { apply canonS_LT. - apply (LT_nf_r H0). - intro;subst; destruct n0;auto. } Qed.
imports: hydras(DecPreOrder Canon MoreLists First_toggle OrdNotations) Coq(Lia)