proposition: Lemma Regles_inv2 : forall (X V R : Ensf) (x : Elt) (u : Word), Regles X V R -> dans (couple x (word u)) R -> inmonoid (union X V) u.
proof: Proof. intros X V R x u Regles_R dans_couple_R. cut (ex2 (fun A : Elt => dans A V) (fun A : Elt => ex2 (fun B : Word => couple x (word u) = couple A (word B)) (fun B : Word => inmonoid (union X V) B))). intro temp; elim temp; clear temp. intros x0 dans_x0_V temp; elim temp; clear temp. intros u0 eg_couple inmonoid_u0. replace u with u0; prolog [ sym_equal couple_couple_inv2 word_word_inv ] 4. auto. Qed.
imports: Ensf Words more_words need fonctions Relations