proposition: Lemma gnaw_succ: forall alpha i s, nf alpha -> gnaw (T1.succ alpha) (S i::s) = gnaw alpha s.
proof: Proof. intros; cbn; now rewrite canon_succ. Qed.
imports: hydras(DecPreOrder Canon MoreLists First_toggle OrdNotations) Coq(Lia)