proposition: Lemma small_lemma (i:nat) (beta : T1) : forall alpha, const_pathS i alpha beta -> nf alpha -> beta t1<= canon alpha (S i).
proof: Proof. destruct (T1_eq_dec beta zero). - subst; intros; apply LE_zero; auto with T1. apply nf_canon; auto with T1. - induction 1. + intros; destruct H; subst. apply LE_refl. auto with T1. apply nf_canon; auto with T1. + destruct H; subst; intro; apply LE_trans with (canon (canon x (S i)) (S i)). * apply IHclos_trans_1n; auto. apply nf_canon; auto. * apply LE_r, canonS_LT. { apply nf_canon; auto. } { intro H2. rewrite H2 in H0. apply const_pathS_zero in H0. now destruct n. } Qed.
imports: hydras(DecPreOrder Canon MoreLists First_toggle OrdNotations) Coq(Lia)