Let net, sub, J, leJ, K, leK, X and phi be given.

Assume H: subnet_of_witness net sub J leJ K leK X phi.

We will prove directed_set K leK.

Apply H to the current goal.

Assume Hcore13 Hvals.

Apply Hcore13 to the current goal.

Assume Hcore12 Hcofinal.

Apply Hcore12 to the current goal.

Assume Hcore11 Hmono.

Apply Hcore11 to the current goal.

Assume Hcore10 Hdomphi.

Apply Hcore10 to the current goal.

Assume Hcore9 Hgraphphi.

Apply Hcore9 to the current goal.

Assume Hcore8 Htotphi.

Apply Hcore8 to the current goal.

Assume Hcore7 Hdomsub.

Apply Hcore7 to the current goal.

Assume Hcore6 Hgraphsub.

Apply Hcore6 to the current goal.

Assume Hcore5 Htotsub.

Apply Hcore5 to the current goal.

Assume Hcore4 Hdomnet.

Apply Hcore4 to the current goal.

Assume Hcore3 Hgraphnet.

Apply Hcore3 to the current goal.

Assume Hcore2 Htotnet.

Apply Hcore2 to the current goal.

Assume HdirJ HdirK.

An exact proof term for the current goal is HdirK.

∎