proposition: Lemma egalGim'_image_comp : Gim' = imageGram (comp invf f) X V R S :>Ensf * (Ensf * (Ensf * Elt)).
proof: Proof. unfold Gim' in |- *. unfold Sim, Rim, Gim3, Vim, Gim2, Xim, Gim, imageGram in |- *; simpl in |- *. apply pair_equal. rewrite (map_map_eg_map_comp invf f X); auto. apply pair_equal. rewrite (map_map_eg_map_comp invf f V); auto. apply pair_equal. change (map (Rf invf) (map (Rf f) R) = map (Rf (comp invf f)) R :>Ensf) in |- *. replace (map (Rf (comp invf f)) R) with (map (comp (Rf invf) (Rf f)) R). apply map_map_eg_map_comp. apply map_egal. exact (comp_Rf invf f). apply refl_equal. Qed.
imports: Ensf Words more_words need fonctions Relations gram gram2