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