proposition: Lemma inter_X_V1_u_V2 : isGram X V1 R1 S1 -> isGram X V2 R2 S2 -> inter X (union V1 V2) empty.
proof: Proof. prolog [ isGram2 union_inter ] 5. Qed.
imports: Ensf Words more_words Rat need fonctions Relations gram gram2 gram3