proposition: Lemma gnaw_app : forall s s' alpha, gnaw alpha (s ++ s') = gnaw (gnaw alpha s) s'.
proof: Proof. induction s; cbn. - trivial. - destruct a; auto. Qed.
imports: hydras(DecPreOrder Canon MoreLists First_toggle OrdNotations) Coq(Lia)