proposition: Lemma inter_X_Vu : isGram X V1 R1 S1 -> isGram X V2 R2 S2 -> inter X Vu empty.
proof: Proof. intro G1. intro G2. unfold Vu in |- *. unfold C in |- *. unfold Gunion in |- *. simpl in |- *. apply union_inter. apply isGram2 with R1 S1; assumption. apply isGram2 with R2 S2; assumption. Qed.
imports: Ensf Words more_words need fonctions Relations gram