proposition: Lemma standard_path_to_nf : forall i alpha j beta, standard_path_to j beta i alpha -> nf alpha -> nf beta.
proof: Proof. induction 1. - destruct i. now destruct H2. + subst beta; intros; now apply nf_canon. - intros; apply IHstandard_path_to. destruct i. + simpl;auto with T1. now apply nf_canon. + unfold canon; now apply nf_canon. Qed.
imports: hydras(DecPreOrder Canon MoreLists First_toggle OrdNotations) Coq(Lia)