Let X, N and S be given.
Assume HNS: subnet_pack_of_in X N S.
We will prove subnet_pack_of_in X N N.
We prove the intermediate claim HsubDef: subnet_pack_of_in X N N = ∃phi0 : set, subnet_of_witness (net_pack_fun N) (net_pack_fun N) (net_pack_index N) (net_pack_le N) (net_pack_index N) (net_pack_le N) X phi0.
Use reflexivity.
rewrite the current goal using HsubDef (from left to right).
Apply HNS 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.
We prove the intermediate claim HdirN: directed_set (net_pack_index N) (net_pack_le N).
An exact proof term for the current goal is (subnet_of_witness_dirJ (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).
We prove the intermediate claim HtotN: total_function_on (net_pack_fun N) (net_pack_index N) X.
An exact proof term for the current goal is (subnet_of_witness_totnet (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).
We prove the intermediate claim HgraphN: functional_graph (net_pack_fun N).
An exact proof term for the current goal is (subnet_of_witness_graphnet (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).
We prove the intermediate claim HdomN: graph_domain_subset (net_pack_fun N) (net_pack_index N).
An exact proof term for the current goal is (subnet_of_witness_domnet (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).
Set idN to be the term {(y,y)|y ∈ net_pack_index N}.
We use idN to witness the existential quantifier.
We will prove subnet_of_witness (net_pack_fun N) (net_pack_fun N) (net_pack_index N) (net_pack_le N) (net_pack_index N) (net_pack_le N) X idN.
We prove the intermediate claim HwitDef: subnet_of_witness (net_pack_fun N) (net_pack_fun N) (net_pack_index N) (net_pack_le N) (net_pack_index N) (net_pack_le N) X idN = (directed_set (net_pack_index N) (net_pack_le N) ∧ directed_set (net_pack_index N) (net_pack_le N) ∧ total_function_on (net_pack_fun N) (net_pack_index N) X ∧ functional_graph (net_pack_fun N) ∧ graph_domain_subset (net_pack_fun N) (net_pack_index N) ∧ total_function_on (net_pack_fun N) (net_pack_index N) X ∧ functional_graph (net_pack_fun N) ∧ graph_domain_subset (net_pack_fun N) (net_pack_index N) ∧ total_function_on idN (net_pack_index N) (net_pack_index N) ∧ functional_graph idN ∧ graph_domain_subset idN (net_pack_index N) ∧ (∀i j : set, i ∈ (net_pack_index N) → j ∈ (net_pack_index N) → (i,j) ∈ (net_pack_le N) → (apply_fun idN i,apply_fun idN j) ∈ (net_pack_le N)) ∧ (∀j : set, j ∈ (net_pack_index N) → ∃k : set, k ∈ (net_pack_index N) ∧ (j,apply_fun idN k) ∈ (net_pack_le N)) ∧ (∀k : set, k ∈ (net_pack_index N) → apply_fun (net_pack_fun N) k = apply_fun (net_pack_fun N) (apply_fun idN k))).
Use reflexivity.
rewrite the current goal using HwitDef (from left to right).
Apply and14I to the current goal.
An exact proof term for the current goal is HdirN.
An exact proof term for the current goal is HdirN.
An exact proof term for the current goal is HtotN.
An exact proof term for the current goal is HgraphN.
An exact proof term for the current goal is HdomN.
An exact proof term for the current goal is HtotN.
An exact proof term for the current goal is HgraphN.
An exact proof term for the current goal is HdomN.
An exact proof term for the current goal is (identity_total_function_on (net_pack_index N)).
An exact proof term for the current goal is (functional_graph_graph (net_pack_index N) (λy : set ⇒ y)).
An exact proof term for the current goal is (graph_domain_subset_graph (net_pack_index N) (λy : set ⇒ y)).
Let i and j be given.
Assume Hi: i ∈ net_pack_index N.
Assume Hj: j ∈ net_pack_index N.
Assume Hij: (i,j) ∈ net_pack_le N.
We will prove (apply_fun idN i,apply_fun idN j) ∈ net_pack_le N.
rewrite the current goal using (identity_function_apply (net_pack_index N) i Hi) (from left to right).
rewrite the current goal using (identity_function_apply (net_pack_index N) j Hj) (from left to right).
An exact proof term for the current goal is Hij.
Let j be given.
Assume Hj: j ∈ net_pack_index N.
We use j to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hj.
We prove the intermediate claim Hrefl: (j,j) ∈ net_pack_le N.
An exact proof term for the current goal is (directed_set_refl (net_pack_index N) (net_pack_le N) HdirN j Hj).
rewrite the current goal using (identity_function_apply (net_pack_index N) j Hj) (from left to right).
An exact proof term for the current goal is Hrefl.
Let k be given.
Assume Hk: k ∈ net_pack_index N.
rewrite the current goal using (identity_function_apply (net_pack_index N) k Hk) (from left to right).
Use reflexivity.
∎