proposition: Lemma comp_Word_ext : forall f g : Elt -> Elt, eg_f_W_W (Word_ext (comp f g)) (comp_word (Word_ext f) (Word_ext g)).
proof: Proof. intros f g. unfold eg_f_W_W, Word_ext, comp, comp_word in |- *. simple induction x; simpl in |- *; auto. Qed.
imports: Ensf Words more_words need