proposition: Lemma Derive_P_A_2_inv : forall x y : Conf, Derive_P_A_2 x y -> Derive_P_A_2_nind x y.
proof: Proof. intros x y Der. unfold Derive_P_A_2_nind in |- *. elim Der. intros w u x0 dans_x0_X. apply or_introl. exists x0; auto. intros v w u x0 dans_couple_Der. apply or_intror. exists x0. exists w. auto. exists u; auto. Qed.
imports: Ensf Words more_words need Relations gram gram_g PushdownAutomata