Let z be given.
We will
prove z ∈ pair x y.
An
exact proof term for the current goal is
(lamE 2 (λi ⇒ if i = 0 then x else y) z Hz).
Let i be given.
Let w be given.
We will
prove z ∈ pair x y.
rewrite the current goal using H2 (from left to right).
We will
prove pair i w ∈ pair x y.
We prove the intermediate
claim L2:
i ∈ {0,1}.
Apply (UPairE i 0 1 L2) to the current goal.
rewrite the current goal using Hi0 (from left to right).
We will
prove pair 0 w ∈ pair x y.
Apply pairI0 to the current goal.
We prove the intermediate
claim L3:
(if i = 0 then x else y) = x.
An
exact proof term for the current goal is
(If_i_1 (i = 0) x y Hi0).
rewrite the current goal using L3 (from right to left).
An exact proof term for the current goal is Hw.
rewrite the current goal using Hi1 (from left to right).
We will
prove pair 1 w ∈ pair x y.
Apply pairI1 to the current goal.
We prove the intermediate
claim L3:
(if i = 0 then x else y) = y.
rewrite the current goal using Hi1 (from left to right).
rewrite the current goal using L3 (from right to left).
An exact proof term for the current goal is Hw.
∎