fact: Definition Regles (X V R : Ensf) := forall x : Elt, dans x R -> ex2 (fun A : Elt => dans A V) (fun A : Elt => ex2 (fun B : Word => x = couple A (word B)) (fun B : Word => inmonoid (union X V) B)).
imports: Ensf Words more_words need fonctions Relations