Let X, Tx, N and x be given.

Assume H: net_pack_converges X Tx N x.

We will prove x ∈ X.

Apply H to the current goal.

Let J be given.

Assume Hexle: ∃le net : set, N = net_pack J le net ∧ net_converges_on X Tx net J le x.

Apply Hexle to the current goal.

Let le be given.

Assume Hexnet: ∃net : set, N = net_pack J le net ∧ net_converges_on X Tx net J le x.

Apply Hexnet to the current goal.

Let net be given.

Assume Hpair: N = net_pack J le net ∧ net_converges_on X Tx net J le x.

We prove the intermediate claim Hconv: net_converges_on X Tx net J le x.

An exact proof term for the current goal is (andER (N = net_pack J le net) (net_converges_on X Tx net J le x) Hpair).

Apply Hconv to the current goal.

Assume Hcore Htail.

Apply Hcore to the current goal.

Assume Hcore5 HxX.

An exact proof term for the current goal is HxX.

∎