proposition: Lemma is_iso_f_imp_Id_words_weinvf_wef : is_iso E F f -> Id_words E weinvf_wef.
proof: Proof. intro is_iso_f. red in |- *. intro x. unfold weinvf_wef, weinvf, wef in |- *. cut (eg_f_W_W (Word_ext (comp invf' f)) (comp_word (Word_ext invf') (Word_ext f))). unfold eg_f_W_W in |- *. intro Hyp. rewrite <- (Hyp x). generalize x. change (Id_words E (Word_ext (comp invf' f))) in |- *. apply extension_Id. unfold invf' in |- *. auto. auto. Qed.
imports: Ensf Words more_words need