An exact proof term for the current goal is (andER ((topology_on X Tx ∧ topology_on Y Ty) ∧ total_function_on f X Y) (∀V : set, V ∈ Ty → preimage_of X f V ∈ Tx) H).