proposition: Lemma Derive_P_A_2_imp_Derive_P_A_3 : forall (s : Word) (x y : Conf), Derive_P_A_2 x y -> exists s2 : Word, Derive_P_A_3 (s, x) (s2, y).
proof: Proof. intros s x y Derive_P_A_2_x_y. elim Derive_P_A_2_x_y. intros w u x0 dans_x0_X. exists (Append s (cons x0 nil)). apply Derive3_X; assumption. intros v w u x0 dans_couple. intros; exists s. apply Derive3_V; assumption. Qed.
imports: Ensf Words more_words need Relations gram gram_g PushdownAutomata