Let X, N, J, le and net be given.
Assume H: net_pack_in_space X N.
Assume HNdef: N = net_pack J le net.
Apply H to the current goal.
Let J0 be given.
Assume Hexle0: ∃le0 net0 : set, N = net_pack J0 le0 net0 ∧ directed_set J0 le0 ∧ total_function_on net0 J0 X ∧ functional_graph net0 ∧ graph_domain_subset net0 J0.
Apply Hexle0 to the current goal.
Let le0 be given.
Assume Hexnet0: ∃net0 : set, N = net_pack J0 le0 net0 ∧ directed_set J0 le0 ∧ total_function_on net0 J0 X ∧ functional_graph net0 ∧ graph_domain_subset net0 J0.
Apply Hexnet0 to the current goal.
Let net0 be given.
Assume Hdata: N = net_pack J0 le0 net0 ∧ directed_set J0 le0 ∧ total_function_on net0 J0 X ∧ functional_graph net0 ∧ graph_domain_subset net0 J0.
Apply (and5E (N = net_pack J0 le0 net0) (directed_set J0 le0) (total_function_on net0 J0 X) (functional_graph net0) (graph_domain_subset net0 J0) Hdata) to the current goal.
Assume HN0 Hdir0 Htot0 Hgraph0 Hdom0.
We prove the intermediate claim HeqPack: net_pack J le net = net_pack J0 le0 net0.
rewrite the current goal using HNdef (from right to left).
An exact proof term for the current goal is HN0.
We prove the intermediate claim HJeq: J = J0.
We prove the intermediate claim Hidx: net_pack_index (net_pack J le net) = net_pack_index (net_pack J0 le0 net0).
rewrite the current goal using HeqPack (from left to right).
Use reflexivity.
We will prove J = J0.
rewrite the current goal using (net_pack_index_eq J le net) (from right to left).
rewrite the current goal using (net_pack_index_eq J0 le0 net0) (from right to left).
An exact proof term for the current goal is Hidx.
We prove the intermediate claim Hleeq: le = le0.
We prove the intermediate claim Hle: net_pack_le (net_pack J le net) = net_pack_le (net_pack J0 le0 net0).
rewrite the current goal using HeqPack (from left to right).
Use reflexivity.
We will prove le = le0.
rewrite the current goal using (net_pack_le_eq J le net) (from right to left).
rewrite the current goal using (net_pack_le_eq J0 le0 net0) (from right to left).
An exact proof term for the current goal is Hle.
We prove the intermediate claim Hnete: net = net0.
We prove the intermediate claim Hf: net_pack_fun (net_pack J le net) = net_pack_fun (net_pack J0 le0 net0).
rewrite the current goal using HeqPack (from left to right).
Use reflexivity.
We will prove net = net0.
rewrite the current goal using (net_pack_fun_eq J le net) (from right to left).
rewrite the current goal using (net_pack_fun_eq J0 le0 net0) (from right to left).
An exact proof term for the current goal is Hf.
rewrite the current goal using HJeq (from left to right).
rewrite the current goal using Hleeq (from left to right).
rewrite the current goal using Hnete (from left to right).
An exact proof term for the current goal is (and4I (directed_set J0 le0) (total_function_on net0 J0 X) (functional_graph net0) (graph_domain_subset net0 J0) Hdir0 Htot0 Hgraph0 Hdom0).
∎