proposition: Lemma is_epi_f_imp_is_epi_words : is_epi E F f -> is_epi_words E F wef.
proof: Proof. intro temp; elim temp; clear temp. intro application_f. intro is_epi_f. split. auto. simple induction x; clear x. exists nil; auto. intros x w Hyp inmonoid_F_cons. cut (exists2 y : Word, w = wef y & inmonoid E y). intro temp; elim temp; clear temp. intros y1 y1_egal inmonoid_y1. cut (exists2 x_ant : Elt, x = f x_ant & dans x_ant E). intro temp; elim temp; clear temp. intros x_ant x_egal dans_x_ant. exists (cons x_ant y1). unfold wef, Word_ext in |- *. auto. auto. prolog [ inmonoid_cons_inv2 ] 3. prolog [ inmonoid_cons_inv ] 3. Qed.
imports: Ensf Words more_words need