proposition: Lemma weinvf_wef : Id_words (union X V) (comp_word weinvf wef).
proof: Proof. unfold Id_words in |- *. unfold weinvf, wef in |- *. intro x. rewrite <- (comp_Word_ext invf f x). generalize x. apply (extension_Id (union X V) (comp invf f)). exact invf_f. Qed.
imports: Ensf Words more_words need fonctions Relations gram gram2