proposition: Lemma N_dans_S_X : ~ dans S' X.
proof: Proof. red in |- *. intro dans_S_X. elimtype (exists w : Word, word w = S'). intro x. change (word x <> natural 0) in |- *. discriminate. apply Mots_X; assumption. Qed.
imports: Ensf Words more_words Rat need fonctions Relations gram gram2 gram3 gram4