Let X, N, S1 and S2 be given.
Assume HNS1: subnet_pack_of_in X N S1.
Assume HNS2: subnet_pack_of_in X N S2.
We will prove ∃R : set, subnet_pack_of_in X N R ∧ subnet_pack_of_in X R S1 ∧ subnet_pack_of_in X R S2.
We use N to witness the existential quantifier.
Apply and3I to the current goal.
An exact proof term for the current goal is (subnet_pack_of_in_refl_from_subnet X N S1 HNS1).
An exact proof term for the current goal is HNS1.
An exact proof term for the current goal is HNS2.
∎