proposition: Lemma inv_is_epi : is_iso E F f -> is_epi F E invf.
proof: Proof. unfold invf in |- *. intro is_iso_f. split. auto. intros x dans_x. exists (f x); [ apply sym_equal; auto | elim is_iso_f ]. intros is_epi_f. elim is_epi_f. auto. Qed.
imports: Ensf Words more_words need