proposition: Lemma is_mono_f_imp_is_mono_words : is_mono E f -> is_mono_words E wef.
proof: Proof. intro Hyp. red in |- *. simple induction x. intros. apply sym_equal. apply wef_nil with f. auto. intros x0 w0. intros. cut (exists x : Elt, (exists2 w : Word, cons x w = y & f x = f x0 /\ wef w = wef w0)). intro temp; elim temp; clear temp. intro e. intro temp; elim temp; clear temp. intro r. intros y_egal temp. elim temp; clear temp. intros. rewrite <- y_egal. apply cons_cons. apply Hyp. apply inmonoid_cons_inv2 with w0; assumption. apply inmonoid_cons_inv2 with r; rewrite y_egal; assumption. auto. apply H. apply (inmonoid_cons_inv E w0 x0); assumption. apply (inmonoid_cons_inv E r e); rewrite y_egal; assumption. auto. unfold wef in |- *. auto. Qed.
imports: Ensf Words more_words need