Let net1, net2, sub1, sub2, J1, J2, leJ1, leJ2, K1, K2, leK1, leK2, X and phi be given.

Assume Hnet: net1 = net2.

Assume Hsub: sub1 = sub2.

Assume HJ: J1 = J2.

Assume HleJ: leJ1 = leJ2.

Assume HK: K1 = K2.

Assume HleK: leK1 = leK2.

Assume H: subnet_of_witness net1 sub1 J1 leJ1 K1 leK1 X phi.

rewrite the current goal using Hnet (from right to left).

rewrite the current goal using Hsub (from right to left).

rewrite the current goal using HJ (from right to left).

rewrite the current goal using HleJ (from right to left).

rewrite the current goal using HK (from right to left).

rewrite the current goal using HleK (from right to left).

An exact proof term for the current goal is H.

∎