Let x0 of type ι be given.
Let x1 of type ι be given.
Let x2 of type ι be given.
Assume H0: x0 = x1 ⟶ ∀ x3 : ο . x3.
Assume H1: x0 = x2 ⟶ ∀ x3 : ο . x3.
Assume H2: x1 = x2 ⟶ ∀ x3 : ο . x3.
Apply equip_sym with
u3,
SetAdjoin (UPair x0 x1) x2.
Apply unknownprop_eab190d6552dbda6c7d00c3e93c1ad9385698a8d73462a2a4e5795b67701610d with
u2,
UPair x0 x1,
x2 leaving 2 subgoals.
Assume H3:
x2 ∈ UPair x0 x1.
Apply UPairE with
x2,
x0,
x1,
False leaving 3 subgoals.
The subproof is completed by applying H3.
Assume H4: x2 = x0.
Apply H1.
Let x3 of type ι → ι → ο be given.
The subproof is completed by applying H4 with λ x4 x5 . x3 x5 x4.
Assume H4: x2 = x1.
Apply H2.
Let x3 of type ι → ι → ο be given.
The subproof is completed by applying H4 with λ x4 x5 . x3 x5 x4.
Apply equip_sym with
UPair x0 x1,
u2.
Apply unknownprop_39df499f773ced696ac600b0767cd28b9ceea72e50ff2c9103bc16896281c585 with
x0,
x1.
The subproof is completed by applying H0.