proposition: Lemma inter_X_Vu_d : isGram X V1 R1 S1 -> isGram X V2 R2 S2 -> ~ dans S X -> inter X Vu empty.
proof: Proof. intros G_1 G_2 N_dans_S_X. unfold inter in |- *. split. auto. split. auto. intros x dans_x_X dans_x_Vu. absurd (dans x X). cut (S = x :>Elt \/ dans x (union V1 V2)). intro temp; elim temp; clear temp. intros egal_S_x. rewrite <- egal_S_x; assumption. intro dans_x_V1_u_V2. prolog [ inter_X_V1_u_V2 sym_inter inter_dans ] 4. auto. assumption. Qed.
imports: Ensf Words more_words Rat need fonctions Relations gram gram2 gram3