Let X, Tx, N and x be given.
Assume H: net_pack_converges X Tx N x.
We will prove net_converges X Tx (net_pack_fun N) 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 HN: N = net_pack J le net.
An exact proof term for the current goal is (andEL (N = net_pack J le net) (net_converges_on X Tx net J le x) Hpair).
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).
rewrite the current goal using HN (from left to right).
rewrite the current goal using (net_pack_fun_eq J le net) (from left to right).
An exact proof term for the current goal is (net_converges_on_implies_net_converges X Tx net J le x Hconv).
∎