proposition: Lemma Derive_image : forall u v : Word, Derive R1 u v -> Derive Rim (wef u) (wef v).
proof: Proof. intros u v H. elim H; clear H u v. intros u v A dans_A. replace (wef (cons A v)) with (cons (f A) (wef v)). replace (wef (Append u v)) with (Append (wef u) (wef v)). auto. apply sym_equal; unfold wef in |- *; apply wef_append; auto. auto. intros. replace (wef (cons x u)) with (cons (f x) (wef u)). replace (wef (cons x v)) with (cons (f x) (wef v)); auto. auto. Qed.
imports: Ensf Words more_words need fonctions Relations gram