proposition: Lemma gnawS_succ_eqn2 : forall i n s gamma, nf gamma -> gnawS (T1.cons (T1.succ gamma) (S n) zero) (i::s) = gnawS (T1.cons (T1.succ gamma) n (T1.cons gamma i T1.zero)) s.
proof: Proof. intros; rewrite gnaws_rw. rewrite canonS_cons_succ_eqn2; auto. Qed.
imports: hydras(DecPreOrder Canon MoreLists First_toggle OrdNotations) Coq(Lia)