proposition: Lemma Regles_inv1 : forall (X V R : Ensf) (x y : Elt), Regles X V R -> dans (couple x y) R -> dans x V.
proof: Proof. intros X V R x y Regles_R dans_couple_R. cut (ex2 (fun A : Elt => dans A V) (fun A : Elt => ex2 (fun B : Word => couple x y = 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 u eg_couple inmonoid_u. replace x with x0; prolog [ sym_equal couple_couple_inv1 ] 3. auto. Qed.
imports: Ensf Words more_words need fonctions Relations