proposition: Lemma gnawS_nf : forall s alpha, nf alpha -> nf (gnawS alpha s).
proof: Proof. induction s. - intros; now cbn. - intros; cbn; apply IHs; apply nf_canon;auto. Qed.
imports: hydras(DecPreOrder Canon MoreLists First_toggle OrdNotations) Coq(Lia)