proposition: Lemma isGram_inclus2 : forall (X V R R' : Ensf) (S : Elt), inclus R' R -> isGram X V R S -> isGram X V R' S.
proof: Proof. prolog [ isGram4 Regles_R isGram3 isGram2 isGram1 isGram5 ] 11. Qed.
imports: Ensf Words more_words need fonctions Relations