proposition: Lemma path_toS_nf beta s alpha: path_toS beta s alpha -> nf alpha -> nf beta.
proof: Proof. induction 1. - destruct H; subst; intro; now apply nf_canon. - intro; apply IHpath_toS; auto. destruct H; subst; now apply nf_canon. Qed.
imports: hydras(DecPreOrder Canon MoreLists First_toggle OrdNotations) Coq(Lia)