proposition: Lemma Deriveg_imp_Deriveg_App_2 : forall x y a : Word, inmonoid X a -> Deriveg X R x y -> Deriveg X R (Append a x) (Append a y).
proof: Proof. intros x y. simple induction a. auto. intros x0 w Hyp inmonoid_X_cons_x0_w Der_x_y. change (Deriveg X R (cons x0 (Append w x)) (cons x0 (Append w y))) in |- *. apply Deriveg2. apply inmonoid_cons_inv2 with w; assumption. apply Hyp. apply inmonoid_cons_inv with x0; assumption. assumption. Qed.
imports: Ensf Words more_words need Relations gram gram_g PushdownAutomata