proposition: Lemma gnawS_SSn (i:nat) s : forall alpha n , nf alpha -> gnawS (T1.cons alpha (S n) T1.zero) (i::s) = gnawS (T1.cons alpha n (canon (T1.cons alpha 0 zero) (S i))) s.
proof: Proof. intros. rewrite gnaws_rw; auto. rewrite canon_SSn_zero; auto. Qed.
imports: hydras(DecPreOrder Canon MoreLists First_toggle OrdNotations) Coq(Lia)