proposition: Lemma const_pathS_nf : forall n alpha beta, const_pathS n alpha beta -> nf alpha -> nf beta.
proof: Proof. induction 1. - destruct H; subst; intro; apply nf_canon;auto. - intro; apply IHclos_trans_1n; subst. destruct H. subst; apply nf_canon;auto. Qed.
imports: hydras(DecPreOrder Canon MoreLists First_toggle OrdNotations) Coq(Lia)