proposition: Lemma image_isGram : isGram X V1 R1 S1 -> Mots Xim -> inter Xim Vim empty -> isGram Xim Vim Rim Sim.
proof: Proof. unfold Sim, Rim, Gim3, Vim, Gim2, Xim, Gim, imageGram in |- *; simpl in |- *. prolog [ isGram4 image_Regles isGram3 dans_map_inv isGram5 ] 7. Qed.
imports: Ensf Words more_words need fonctions Relations gram