Let x0 of type ι be given.
Apply Empty_Subq_eq with
ap 0 x0.
Let x1 of type ι be given.
Claim L1:
lam 2 (λ x2 . If_i (x2 = 0) x0 x1) ∈ 0Apply apE2 with
0,
x0,
x1.
The subproof is completed by applying H0.
Apply EmptyE with
lam 2 (λ x2 . If_i (x2 = 0) x0 x1),
x1 ∈ 0.
The subproof is completed by applying L1.