proposition: Lemma Derive_P_A_3_conserve_inmonoid_s : forall x y x' y' s s' : Word, Derive_P_A_3 (s, (x, y)) (s', (x', y')) -> inmonoid X s -> inmonoid X s'.
proof: Proof. intros x y x' y' s s' Der. change ((fun a a' : Word * Conf => inmonoid X (fst a) -> inmonoid X (fst a')) (s, (x, y)) (s', (x', y'))) in |- *. elim Der; simpl in |- *. intros. apply inmonoid_Append; auto. auto. Qed.
imports: Ensf Words more_words need Relations gram gram_g PushdownAutomata