Let net and sub be given.

Assume Hsub: subnet_of net sub.

We will prove net_on sub.

Apply Hsub to the current goal.

Let J be given.

Assume Hex1.

Apply Hex1 to the current goal.

Let leJ be given.

Assume Hex2.

Apply Hex2 to the current goal.

Let K be given.

Assume Hex3.

Apply Hex3 to the current goal.

Let leK be given.

Assume Hex4.

Apply Hex4 to the current goal.

Let X be given.

Assume Hex5.

Apply Hex5 to the current goal.

Let phi be given.

Assume Hall.

We will prove ∃J0 le0 X0 : set, directed_set J0 le0 ∧ total_function_on sub J0 X0 ∧ functional_graph sub ∧ graph_domain_subset sub J0.

We use K to witness the existential quantifier.

We use leK to witness the existential quantifier.

We use X to witness the existential quantifier.

We will prove directed_set K leK ∧ total_function_on sub K X ∧ functional_graph sub ∧ graph_domain_subset sub K.

Apply Hall to the current goal.

Assume H13 Hvals.

Apply H13 to the current goal.

Assume H12 Hcofinal.

Apply H12 to the current goal.

Assume H11 Hmono.

Apply H11 to the current goal.

Assume H10 Hdomphi.

Apply H10 to the current goal.

Assume H9 Hdomsub.

Apply H9 to the current goal.

Assume H8 Hdomnet.

Apply H8 to the current goal.

Assume H7 Hgraphphi.

Apply H7 to the current goal.

Assume H6 Htotphi.

Apply H6 to the current goal.

Assume H5 Hgraphsub.

Apply H5 to the current goal.

Assume H4 Htotsub.

Apply H4 to the current goal.

Assume H3 Hgraphnet.

Apply H3 to the current goal.

Assume H2 Htotnet.

Apply H2 to the current goal.

Assume HdirJ HdirK.

Apply and4I to the current goal.

An exact proof term for the current goal is HdirK.

An exact proof term for the current goal is Htotsub.

An exact proof term for the current goal is Hgraphsub.

An exact proof term for the current goal is Hdomsub.

∎