Let X, Tx1, Tx2, Y and U be given.
We prove the intermediate
claim Hex:
∃V ∈ Tx1, U = V ∩ Y.
Apply Hex to the current goal.
Let V be given.
Assume HVpair.
We prove the intermediate
claim HV1:
V ∈ Tx1.
An
exact proof term for the current goal is
(andEL (V ∈ Tx1) (U = V ∩ Y) HVpair).
We prove the intermediate
claim HUeq:
U = V ∩ Y.
An
exact proof term for the current goal is
(andER (V ∈ Tx1) (U = V ∩ Y) HVpair).
We prove the intermediate
claim HV2:
V ∈ Tx2.
An exact proof term for the current goal is (Hsub V HV1).
rewrite the current goal using HUeq (from left to right).
∎