Let X and N be given.
Assume H: net_pack_in_space X N.
We will prove net_in_space X (net_pack_fun N).
Apply H to the current goal.
Let J be given.
Assume Hexle: ∃le net : set, N = net_pack J le net ∧ directed_set J le ∧ total_function_on net J X ∧ functional_graph net ∧ graph_domain_subset net J.
Apply Hexle to the current goal.
Let le be given.
Assume Hexnet: ∃net : set, N = net_pack J le net ∧ directed_set J le ∧ total_function_on net J X ∧ functional_graph net ∧ graph_domain_subset net J.
Apply Hexnet to the current goal.
Let net be given.
Assume Hpack: N = net_pack J le net ∧ directed_set J le ∧ total_function_on net J X ∧ functional_graph net ∧ graph_domain_subset net J.
We will prove ∃J0 le0 : set, directed_set J0 le0 ∧ total_function_on (net_pack_fun N) J0 X ∧ functional_graph (net_pack_fun N) ∧ graph_domain_subset (net_pack_fun N) J0.
We use J to witness the existential quantifier.
We use le to witness the existential quantifier.
Apply (and5E (N = net_pack J le net) (directed_set J le) (total_function_on net J X) (functional_graph net) (graph_domain_subset net J) Hpack) to the current goal.
Assume HN Hdir Htot Hgraph Hdom.
rewrite the current goal using HN (from left to right).
rewrite the current goal using (net_pack_fun_eq J le net) (from left to right).
An exact proof term for the current goal is (and4I (directed_set J le) (total_function_on net J X) (functional_graph net) (graph_domain_subset net J) Hdir Htot Hgraph Hdom).
∎