Let net be given.

Assume Hnet: net_on net.

We will prove subnet_of net net.

We prove the intermediate claim Hex: ∃J le X : set, directed_set J le ∧ total_function_on net J X ∧ functional_graph net ∧ graph_domain_subset net J.

An exact proof term for the current goal is Hnet.

Apply Hex to the current goal.

Let J be given.

Assume Hex1.

Apply Hex1 to the current goal.

Let le be given.

Assume Hex2.

Apply Hex2 to the current goal.

Let X be given.

Assume Hall.

Apply Hall to the current goal.

Assume Hleft Hdom.

Apply Hleft to the current goal.

Assume Hleft2 Hgraph.

Apply Hleft2 to the current goal.

Assume Hdir Htot.

An exact proof term for the current goal is (subnet_of_refl_witnessed J le X net Hdir Htot Hgraph Hdom).

∎