proposition: Lemma gnawS_cut1 : forall s alpha n beta, nf (T1.cons alpha n beta) -> gnawS (T1.cons alpha n beta) s = T1.zero -> exists s1 s2, s = s1 ++ s2 /\ gnawS beta s1 = zero /\ gnawS (T1.cons alpha n T1.zero) s2 = zero.
proof: Proof. induction s. - intros. discriminate H0. - intros; assert (nf alpha) by eauto with T1. assert (nf beta) by eauto with T1. destruct (T1_eq_dec beta T1.zero). + subst beta; exists nil, (a::s); repeat split;auto. + rewrite gnaws_rw, canon_tail in H0; auto. destruct (IHs alpha n (canon beta (S a))); auto. * apply nf_intro; auto. apply nf_canon;auto. apply lt_a_phi0_b_phi0R. apply T1.lt_trans with beta. apply canon_lt;auto. apply lt_a_phi0_b_phi0. eapply lt_a_phi0_b_intro; eauto. * destruct H3 as [s2 [H4 [H5 H6]]]; exists (a::x), s2. subst s; split;auto. Qed.
imports: hydras(DecPreOrder Canon MoreLists First_toggle OrdNotations) Coq(Lia)