Let x0 of type ι be given.
Let x1 of type ι be given.
Assume H0: x0 = x1 ⟶ ∀ x2 : ο . x2.
Apply equip_sym with
u2,
UPair x0 x1.
Apply unknownprop_4b1a7ff1f1af5eade46b5657f25a1ce39a3af58e2fba0b757867e511fb9aacae with
x0,
x1,
λ x2 x3 . equip u2 x3.
Apply unknownprop_eab190d6552dbda6c7d00c3e93c1ad9385698a8d73462a2a4e5795b67701610d with
u1,
Sing x0,
x1 leaving 2 subgoals.
Apply H0.
Let x2 of type ι → ι → ο be given.
Apply SingE with
x0,
x1,
λ x3 x4 . x2 x4 x3.
The subproof is completed by applying H1.
Apply equip_sym with
Sing x0,
u1.
The subproof is completed by applying unknownprop_be1ab2772f2343e1b7afd526582f606d68258ba3f0b6521a351e0ecb8bf3c52e with x0.