proposition: Lemma application_imp_application_words : application E F f -> application_words E F wef.
proof: Proof. intro Hyp. red in |- *. intros x inmon; elim inmon; clear inmon. auto. intros. replace (wef (cons e w)) with (cons (f e) (wef w)); auto. Qed.
imports: Ensf Words more_words need