Let X, N, S and T be given.
Assume HNS: subnet_pack_of_in X N S.
Assume HST: subnet_pack_of_in X S T.
We will prove subnet_pack_of_in X N T.
We will prove ∃phi0 : set, subnet_of_witness (net_pack_fun N) (net_pack_fun T) (net_pack_index N) (net_pack_le N) (net_pack_index T) (net_pack_le T) X phi0.
Set Pphi to be the term λphi0 : set ⇒ 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 phi0.
Set phi to be the term Eps_i Pphi.
We prove the intermediate claim Hw1: Pphi phi.
An exact proof term for the current goal is (Eps_i_ex Pphi HNS).
Set Ppsi to be the term λpsi0 : set ⇒ subnet_of_witness (net_pack_fun S) (net_pack_fun T) (net_pack_index S) (net_pack_le S) (net_pack_index T) (net_pack_le T) X psi0.
Set psi to be the term Eps_i Ppsi.
We prove the intermediate claim Hw2: Ppsi psi.
An exact proof term for the current goal is (Eps_i_ex Ppsi HST).
We use (compose_fun (net_pack_index T) psi phi) to witness the existential quantifier.
An exact proof term for the current goal is (subnet_of_witness_trans (net_pack_fun N) (net_pack_fun S) (net_pack_fun T) (net_pack_index N) (net_pack_le N) (net_pack_index S) (net_pack_le S) (net_pack_index T) (net_pack_le T) X phi psi Hw1 Hw2).
∎