proposition: Lemma isGram_inclus3 : forall (X V R : Ensf) (S a : Elt), isGram X V (add a R) S -> isGram X V R S.
proof: Proof. intros X V R S a isGram_X_V_a_R_S. apply isGram_inclus2 with (add a R); auto. Qed.
imports: Ensf Words more_words need fonctions Relations