Let X, d, seq and x be given.
Assume H: sequence_converges_metric X d seq x.
We prove the intermediate claim H123: (metric_on X d ∧ sequence_on seq X) ∧ x ∈ X.
An exact proof term for the current goal is (andEL ((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).
We prove the intermediate claim H12: metric_on X d ∧ sequence_on seq X.
An exact proof term for the current goal is (andEL (metric_on X d ∧ sequence_on seq X) (x ∈ X) H123).
An exact proof term for the current goal is (andER (metric_on X d) (sequence_on seq X) H12).
∎