Let X, N and S be given.

Assume H: subnet_pack_of_in X N S.

We will prove subnet_of (net_pack_fun N) (net_pack_fun S).

Apply H 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_of_witness_implies_subnet_of (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 Hw).

∎