proposition: Lemma gnawS_succ_eqn1 i s gamma : nf gamma -> gnawS (T1.cons (T1.succ gamma) 0 T1.zero) (i::s) = gnawS (T1.cons gamma i T1.zero) s.
proof: Proof. intros; rewrite gnaws_rw. rewrite canonS_phi0_succ_eqn; auto. Qed.
imports: hydras(DecPreOrder Canon MoreLists First_toggle OrdNotations) Coq(Lia)