An exact proof term for the current goal is (andER ((metric_on X d ∧ sequence_on seq X) ∧ x ∈ X) (∀eps : set, eps ∈ R ∧ Rlt 0 eps → ∃N : set, N ∈ ω ∧ ∀n : set, n ∈ ω → N ⊆ n → Rlt (apply_fun d (apply_fun seq n,x)) eps) H).