proposition: Lemma cut_spec : forall u : Word, {a : Word & {b : Word | inmonoid X a /\ Append a b = u /\ (b = nil \/ ex2 (fun x : Elt => ~ dans x X) (fun x : Elt => exists w : Word, b = cons x w))}}.
proof: Proof. intro u. pattern u in |- *. apply Word_rec. exists nil. exists nil. auto. intros x w Hyp. elim Hyp. intros a' spec; elim spec. intros b' temp; elim temp; clear temp. intros inmonoid_a' temp; elim temp; clear temp. intros spec_App spec_or. elimtype ({dans x X} + {~ dans x X}). intro dans_x_X. exists (cons x a'). exists b'. split. apply inmonoid_cons; assumption. split. unfold Append in |- *. simpl in |- *. auto. elim spec_or; intro; assumption. intro N_dans_x_X. exists nil. exists (cons x w). split. auto. split. auto. apply or_intror. exists x. assumption. exists w. apply refl_equal. exact (Dans_spec x X). Qed.
imports: Ensf Words more_words need Relations gram gram_g PushdownAutomata