proposition: Lemma gnaw_gnawS s alpha : gnaw alpha s = gnawS alpha (unshift s).
proof: Proof. revert alpha; induction s; cbn; auto. destruct a as [|i]. - apply IHs. - intros; rewrite IHs. reflexivity. Qed.
imports: hydras(DecPreOrder Canon MoreLists First_toggle OrdNotations) Coq(Lia)