Let X, Tx, N, S and x be given.

Assume Hsub: subnet_pack_of_in X N S.

Assume Hconv: net_converges_on X Tx (net_pack_fun N) (net_pack_index N) (net_pack_le N) x.

We will prove net_converges_on X Tx (net_pack_fun S) (net_pack_index S) (net_pack_le S) x.

Apply Hsub to the current goal.

Let phi be given.

Assume Hw: subnet_of_witness (net_pack_fun N) (net_pack_fun S) (net_pack_index N) (net_pack_le N) (net_pack_index S) (net_pack_le S) X phi.

An exact proof term for the current goal is (subnet_preserves_convergence X Tx (net_pack_fun N) (net_pack_fun S) x (net_pack_index N) (net_pack_le N) (net_pack_index S) (net_pack_le S) phi Hw Hconv).

∎