Let x0 of type ι be given.
Let x1 of type ι be given.
Let x2 of type ι be given.
Let x3 of type ι be given.
Assume H0: x0 = x1 ⟶ ∀ x4 : ο . x4.
Assume H1: x0 = x2 ⟶ ∀ x4 : ο . x4.
Assume H2: x1 = x2 ⟶ ∀ x4 : ο . x4.
Assume H3: x0 = x3 ⟶ ∀ x4 : ο . x4.
Assume H4: x1 = x3 ⟶ ∀ x4 : ο . x4.
Assume H5: x2 = x3 ⟶ ∀ x4 : ο . x4.
Apply unknownprop_eab190d6552dbda6c7d00c3e93c1ad9385698a8d73462a2a4e5795b67701610d with
u3,
SetAdjoin (UPair x0 x1) x2,
x3 leaving 2 subgoals.
Apply unknownprop_434e2e2330a02d70f83efc2b51c595946aeb4462c38cf32d55a1757fe463ba11 with
x0,
x1,
x2,
λ x4 . x4 = x3 ⟶ ∀ x5 : ο . x5,
x3 leaving 5 subgoals.
The subproof is completed by applying H3.
The subproof is completed by applying H4.
The subproof is completed by applying H5.
The subproof is completed by applying H6.
Let x4 of type ι → ι → ο be given.
Assume H7: x4 x3 x3.
The subproof is completed by applying H7.
Apply unknownprop_637144c754e35176e5f73e9789b35a2d801de40f26463f5ae01a3b9c5aad6047 with
x0,
x1,
x2 leaving 3 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
The subproof is completed by applying H2.