proposition: Lemma Reconnait_imageGram : forall w : Word, LG X V1 R1 S1 w -> LG Xim Vim Rim Sim (wef w).
proof: Proof. intro w. unfold LG in |- *. intro temp; split; elim temp; clear temp; intros Der inmo. unfold Sim, Gim3, Gim2, Gim, imageGram in |- *; simpl in |- *. replace (cons (f S1) nil) with (wef (cons S1 nil)); auto. elim inmo. auto. intros wo el. unfold Xim, Gim, imageGram in |- *; simpl in |- *. replace (wef (cons el wo)) with (cons (f el) (wef wo)); auto. Qed.
imports: Ensf Words more_words need fonctions Relations gram