proposition: Lemma extension_Id : forall (E : Ensf) (f : Elt -> Elt), Id E f -> Id_words E (Word_ext f).
proof: Proof. intros E f Id_E_f. red in |- *. simple induction x; clear x. auto. unfold Word_ext in |- *. intros x w Hyp inmonoid_E_cons_x_w. simpl in |- *. apply cons_cons. apply Id_E_f; apply inmonoid_cons_inv2 with w; assumption. apply Hyp. apply inmonoid_cons_inv with x; assumption. Qed.
imports: Ensf Words more_words need