proposition: Lemma gnawS_lim1 (i:nat)(s: list nat) (lambda : T1) : nf lambda -> T1limit lambda -> gnawS (T1.cons lambda 0 T1.zero) (i::s) = gnawS (T1.cons (canon lambda (S i)) 0 T1.zero) s.
proof: Proof. intros; rewrite gnaws_rw. rewrite canonS_lim1; auto. Qed.
imports: hydras(DecPreOrder Canon MoreLists First_toggle OrdNotations) Coq(Lia)