proposition: Lemma inmon_Der_imp_Der : Regles X V1 R1 -> Regles X V2 R2 -> inter (union X V1) V2 empty -> forall u v : Word, Derive Ru u v -> inmonoid (union X V1) u -> Derive R1 u v.
proof: Proof. intros Re_1 Re_2 inter_X_V1_V2_empty u v Der_Ru_u. elim Der_Ru_u. intros u0 v0 A dans_couple_Ru inmon_cons_A_v0. apply Derive1. cut (dans (couple A (word u0)) R1 \/ dans (couple A (word u0)) R2). intro temp; elim temp; clear temp. auto. intro dans_R2. absurd (inter (union X V1) V2 empty). red in |- *. unfold inter in |- *. intro temp; elim temp; clear temp. intros incl_empty_X_V1 temp; elim temp; clear temp. intros incl_empty_V2 imp. apply dans_empty_imp_P with A. apply imp. apply inmonoid_cons_inv2 with v0; assumption. apply Regles_inv1 with X R2 (word u0); assumption. assumption. apply dans_union; assumption. intros u0 v0 x Der_Ru imp inmon_cons_x_u0. apply Derive2. apply imp. apply inmonoid_cons_inv with x. assumption. Qed.
imports: Ensf Words more_words need fonctions Relations gram