proposition: Lemma gnawS_cut2 : forall s alpha n , nf alpha -> gnawS (T1.cons alpha (S n) T1.zero) s = zero -> exists s1 s2, s = s1 ++ s2 /\ gnawS (T1.phi0 alpha) s1 = zero /\ gnawS (T1.cons alpha n T1.zero) s2 = zero.
proof: Proof. destruct s. - intros. discriminate H0. - intros. rewrite gnaws_rw in H0. rewrite canon_SSn_zero in H0; auto. destruct (T1_eq_dec alpha T1.zero). + subst; exists (n::nil), s; split;auto. + destruct (@gnawS_cut1 s alpha n0 (canon (T1.phi0 alpha) (S n))). 2 : auto. rewrite <- canon_SSn_zero; auto. apply nf_canon;auto. * destruct H1 as [s2 [H2 [H3 H4]]];exists (n::x), s2; split;auto. now subst. Qed.
imports: hydras(DecPreOrder Canon MoreLists First_toggle OrdNotations) Coq(Lia)