proposition: Lemma Id_image_S : Id (union X V1) f -> isGram X V1 R1 S1 -> Sim = S1 :>Elt.
proof: Proof. unfold Sim, Gim3, Gim2, Gim, imageGram in |- *; simpl in |- *. prolog [ isGram3 union_d ] 6. Qed.
imports: Ensf Words more_words need fonctions Relations gram