proposition: Lemma cut_Append : forall w : Word, w = Append (cut1 w) (cut2 w).
proof: Proof. intro w. unfold cut1, cut2, cut in |- *. elim (cut_spec w). intros a temp; elim temp; clear temp. intros b temp; elim temp; clear temp. intros inm temp; elim temp. simpl in |- *; auto. Qed.
imports: Ensf Words more_words need Relations gram gram_g PushdownAutomata