Let x0 of type ι be given.
Let x1 of type ι → ι → ο be given.
Assume H0: ∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x0 ⟶ x1 x2 x3 ⟶ x1 x3 x2.
Let x2 of type ι be given.
Assume H2: x2 ∈ x0.
Let x3 of type ι be given.
Assume H3: x3 ∈ x0.
Let x4 of type ι be given.
Assume H4: x4 ∈ x0.
Let x5 of type ι be given.
Assume H5: x5 ∈ x0.
Let x6 of type ι be given.
Assume H6: x6 ∈ x0.
Assume H7: x2 = x3 ⟶ ∀ x7 : ο . x7.
Assume H8: x2 = x4 ⟶ ∀ x7 : ο . x7.
Assume H9: x3 = x4 ⟶ ∀ x7 : ο . x7.
Assume H10: x2 = x5 ⟶ ∀ x7 : ο . x7.
Assume H11: x3 = x5 ⟶ ∀ x7 : ο . x7.
Assume H12: x4 = x5 ⟶ ∀ x7 : ο . x7.
Assume H13: x2 = x6 ⟶ ∀ x7 : ο . x7.
Assume H14: x3 = x6 ⟶ ∀ x7 : ο . x7.
Assume H15: x4 = x6 ⟶ ∀ x7 : ο . x7.
Assume H16: x5 = x6 ⟶ ∀ x7 : ο . x7.
Assume H17: x1 x2 x3.
Assume H18: x1 x2 x4.
Assume H19: x1 x3 x4.
Assume H20: x1 x2 x5.
Assume H21: x1 x3 x5.
Assume H22: x1 x4 x5.
Assume H23: x1 x2 x6.
Assume H24: x1 x3 x6.
Assume H25: x1 x4 x6.
Assume H26: x1 x5 x6.
Apply H1 with
SetAdjoin (SetAdjoin (SetAdjoin (UPair x2 x3) x4) x5) x6 leaving 3 subgoals.
Apply unknownprop_68f81843c4d8e43966ed87e49af6cf26131af8cea5f5f0fd5672255d3a902e96 with
x2,
x3,
x4,
x5,
x6,
λ x7 . x7 ∈ x0 leaving 5 subgoals.
The subproof is completed by applying H2.
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.
Apply equip_atleastp with
u5,
SetAdjoin (SetAdjoin (SetAdjoin (UPair x2 x3) x4) x5) x6.
Apply unknownprop_9781d587d54e97fdc53d81f1412b13d6a13154c4193a0e04448402889fdf7ce2 with
x2,
x3,
x4,
x5,
x6 leaving 10 subgoals.
The subproof is completed by applying H7.
The subproof is completed by applying H8.
The subproof is completed by applying H9.
The subproof is completed by applying H10.
The subproof is completed by applying H11.
The subproof is completed by applying H12.
The subproof is completed by applying H13.
The subproof is completed by applying H14.
The subproof is completed by applying H15.
The subproof is completed by applying H16.
Apply unknownprop_68f81843c4d8e43966ed87e49af6cf26131af8cea5f5f0fd5672255d3a902e96 with
x2,
x3,
x4,
x5,
x6,
λ x7 . ∀ x8 . x8 ∈ SetAdjoin (SetAdjoin (SetAdjoin (UPair x2 x3) x4) x5) x6 ⟶ (x7 = x8 ⟶ ∀ x9 : ο . x9) ⟶ x1 x7 x8 leaving 5 subgoals.
Apply unknownprop_68f81843c4d8e43966ed87e49af6cf26131af8cea5f5f0fd5672255d3a902e96 with
x2,
x3,
x4,
x5,
x6,
λ x7 . (x2 = x7 ⟶ ∀ x8 : ο . x8) ⟶ x1 x2 x7 leaving 5 subgoals.
Assume H27: x2 = x2 ⟶ ∀ x7 : ο . x7.
Apply FalseE with
x1 x2 x2.
Apply H27.
Let x7 of type ι → ι → ο be given.
Assume H28: x7 x2 x2.
The subproof is completed by applying H28.
Assume H27: x2 = x3 ⟶ ∀ x7 : ο . x7.
The subproof is completed by applying H17.
Assume H27: x2 = x4 ⟶ ∀ x7 : ο . x7.
The subproof is completed by applying H18.
Assume H27: x2 = x5 ⟶ ∀ x7 : ο . x7.
The subproof is completed by applying H20.
Assume H27: x2 = x6 ⟶ ∀ x7 : ο . x7.
The subproof is completed by applying H23.
Apply unknownprop_68f81843c4d8e43966ed87e49af6cf26131af8cea5f5f0fd5672255d3a902e96 with
x2,
x3,
x4,
x5,
x6,
λ x7 . (x3 = x7 ⟶ ∀ x8 : ο . x8) ⟶ x1 x3 x7 leaving 5 subgoals.
Assume H27: x3 = x2 ⟶ ∀ x7 : ο . x7.
Apply H0 with
x2,
x3 leaving 3 subgoals.
The subproof is completed by applying H2.
The subproof is completed by applying H3.
The subproof is completed by applying H17.
Assume H27: ... = ... ⟶ ∀ x7 : ο . x7.