proposition: Lemma dans_Rim : forall (A : Elt) (u : Word), dans (couple A (word u)) R1 -> dans (couple (f A) (word (wef u))) Rim.
proof: Proof. intros. unfold Rim, Gim3, Gim2, Gim, imageGram in |- *; simpl in |- *. replace (couple (f A) (word (wef u))) with (fonc (couple A (word u))); auto. Qed.
imports: Ensf Words more_words need fonctions Relations gram