Let X, net, J, le, J' and le' be given.

Assume HJ: directed_set J le ∧ total_function_on net J X ∧ functional_graph net ∧ graph_domain_subset net J.

Assume HJ': directed_set J' le' ∧ total_function_on net J' X ∧ functional_graph net ∧ graph_domain_subset net J'.

Apply (and4E (directed_set J le) (total_function_on net J X) (functional_graph net) (graph_domain_subset net J) HJ) to the current goal.

Assume Hdir Htot Hgraph Hdom.

Apply (and4E (directed_set J' le') (total_function_on net J' X) (functional_graph net) (graph_domain_subset net J') HJ') to the current goal.

Assume Hdir' Htot' Hgraph' Hdom'.

An exact proof term for the current goal is (total_function_on_domain_unique net J J' X Htot Hdom Htot' Hdom').

∎