Let X and net be given.
Assume H: net_in_space X net.
We will prove ∃N : set, net_pack_in_space X N ∧ net_pack_fun N = net.
Apply H to the current goal.
Let J be given.
Assume Hexle: ∃le : set, 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 Hdata: directed_set J le ∧ total_function_on net J X ∧ functional_graph net ∧ graph_domain_subset net J.
We use (net_pack J le net) to witness the existential quantifier.
Apply andI to the current goal.
We will prove net_pack_in_space X (net_pack J le net).
We will prove ∃J0 le0 net0 : set, net_pack J le net = net_pack J0 le0 net0 ∧ directed_set J0 le0 ∧ total_function_on net0 J0 X ∧ functional_graph net0 ∧ graph_domain_subset net0 J0.
We use J to witness the existential quantifier.
We use le to witness the existential quantifier.
We use net to witness the existential quantifier.
Apply (and4E (directed_set J le) (total_function_on net J X) (functional_graph net) (graph_domain_subset net J) Hdata) to the current goal.
Assume Hdir Htot Hgraph Hdom.
Apply (and5I (net_pack J le net = net_pack J le net) (directed_set J le) (total_function_on net J X) (functional_graph net) (graph_domain_subset net J)) to the current goal.
Use reflexivity.
An exact proof term for the current goal is Hdir.
An exact proof term for the current goal is Htot.
An exact proof term for the current goal is Hgraph.
An exact proof term for the current goal is Hdom.
An exact proof term for the current goal is (net_pack_fun_eq J le net).
∎