proposition: Lemma Derive_P_A_2_imp_Der_P_A_2_cons : forall (u : Elt) (x y : Word), Derivestar_P_A_2 (cons u x, y) (nil, nil) -> dans u X -> ex2 (fun w : Word => cons u w = y) (fun w : Word => Derivestar_P_A_2 (x, w) (nil, nil)).
proof: Proof. intros. elimtype (ex2 (fun w : Word => Append (cons u nil) w = y) (fun w : Word => Derivestar_P_A_2 (x, w) (nil, nil))). intros w eg_App Der. exists w; trivial. apply Derive_P_A_2_imp_Der_P_A_2_App with (cons u x); auto. Qed.
imports: Ensf Words more_words need Relations gram gram_g PushdownAutomata