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.
Assume H6: x2 = x3 ⟶ ∀ x6 : ο . x6.
Assume H7: x2 = x4 ⟶ ∀ x6 : ο . x6.
Assume H8: x3 = x4 ⟶ ∀ x6 : ο . x6.
Assume H9: x2 = x5 ⟶ ∀ x6 : ο . x6.
Assume H10: x3 = x5 ⟶ ∀ x6 : ο . x6.
Assume H11: x4 = x5 ⟶ ∀ x6 : ο . x6.
Assume H12: x1 x2 x3.
Assume H13: x1 x2 x4.
Assume H14: x1 x3 x4.
Assume H15: x1 x2 x5.
Assume H16: x1 x3 x5.
Assume H17: x1 x4 x5.
Apply H1 with
SetAdjoin (SetAdjoin (UPair x2 x3) x4) x5 leaving 3 subgoals.
Apply unknownprop_cb75c47bae3a116273752c6fc8e52c777498313f2b5b4ef43d3ceb63348e2717 with
x2,
x3,
x4,
x5,
λ x6 . x6 ∈ x0 leaving 4 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.
Apply equip_atleastp with
u4,
SetAdjoin (SetAdjoin (UPair x2 x3) x4) x5.
Apply unknownprop_1284ca02145609bab9b058960e85f6a8edb5de0340c786fcfde3a88eb0d054c1 with
x2,
x3,
x4,
x5 leaving 6 subgoals.
The subproof is completed by applying H6.
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.
Apply unknownprop_cb75c47bae3a116273752c6fc8e52c777498313f2b5b4ef43d3ceb63348e2717 with
x2,
x3,
x4,
x5,
λ x6 . ∀ x7 . x7 ∈ SetAdjoin (SetAdjoin (UPair x2 x3) x4) x5 ⟶ (x6 = x7 ⟶ ∀ x8 : ο . x8) ⟶ x1 x6 x7 leaving 4 subgoals.
Apply unknownprop_cb75c47bae3a116273752c6fc8e52c777498313f2b5b4ef43d3ceb63348e2717 with
x2,
x3,
x4,
x5,
λ x6 . (x2 = x6 ⟶ ∀ x7 : ο . x7) ⟶ x1 x2 x6 leaving 4 subgoals.
Assume H18: x2 = x2 ⟶ ∀ x6 : ο . x6.
Apply FalseE with
x1 x2 x2.
Apply H18.
Let x6 of type ι → ι → ο be given.
Assume H19: x6 x2 x2.
The subproof is completed by applying H19.
Assume H18: x2 = x3 ⟶ ∀ x6 : ο . x6.
The subproof is completed by applying H12.
Assume H18: x2 = x4 ⟶ ∀ x6 : ο . x6.
The subproof is completed by applying H13.
Assume H18: x2 = x5 ⟶ ∀ x6 : ο . x6.
The subproof is completed by applying H15.
Apply unknownprop_cb75c47bae3a116273752c6fc8e52c777498313f2b5b4ef43d3ceb63348e2717 with
x2,
x3,
x4,
x5,
λ x6 . (x3 = x6 ⟶ ∀ x7 : ο . x7) ⟶ x1 x3 x6 leaving 4 subgoals.
Assume H18: x3 = x2 ⟶ ∀ x6 : ο . x6.
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 H12.
Assume H18: x3 = x3 ⟶ ∀ x6 : ο . x6.
Apply FalseE with
x1 x3 x3.
Apply H18.
Let x6 of type ι → ι → ο be given.
Assume H19: x6 x3 x3.
The subproof is completed by applying H19.
Assume H18: x3 = x4 ⟶ ∀ x6 : ο . x6.
The subproof is completed by applying H14.
Assume H18: x3 = x5 ⟶ ∀ x6 : ο . x6.
The subproof is completed by applying H16.
Apply unknownprop_cb75c47bae3a116273752c6fc8e52c777498313f2b5b4ef43d3ceb63348e2717 with
x2,
x3,
x4,
x5,
λ x6 . (x4 = x6 ⟶ ∀ x7 : ο . x7) ⟶ x1 x4 x6 leaving 4 subgoals.
Assume H18: x4 = x2 ⟶ ∀ x6 : ο . x6.
Apply H0 with
x2,
x4 leaving 3 subgoals.
The subproof is completed by applying H2.
The subproof is completed by applying H4.
The subproof is completed by applying H13.
Assume H18: x4 = x3 ⟶ ∀ x6 : ο . x6.
Apply H0 with
x3,
x4 leaving 3 subgoals.
The subproof is completed by applying H3.
The subproof is completed by applying H4.
The subproof is completed by applying H14.
Assume H18: x4 = ... ⟶ ∀ x6 : ο . x6.