Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Assume H0: x0 ∈ setminus u11 u6.
Let x1 of type ι → ο be given.
Assume H1: x1 u6.
Assume H2: x1 u7.
Assume H3: x1 u8.
Assume H4: x1 u9.
Assume H5: x1 u10.
Apply setminusE with u11, u6, x0, x1 x0 leaving 2 subgoals.
The subproof is completed by applying H0.
Assume H6: x0 ∈ u11.
Assume H7: nIn x0 u6.
Apply unknownprop_0fab5122556b271f6fd5ccb0ad45cb01192affd855cb92d430b4ab8c0e6f785a with x0, λ x2 . x0 = x2 ⟶ x1 x2 leaving 8 subgoals.
Apply setminusI with u12, u6, x0 leaving 2 subgoals.
Apply ordsuccI1 with u11, x0.
The subproof is completed by applying H6.
The subproof is completed by applying H7.
Assume H8: x0 = u6.
The subproof is completed by applying H1.
Assume H8: x0 = u7.
The subproof is completed by applying H2.
Assume H8: x0 = u8.
The subproof is completed by applying H3.
Assume H8: x0 = u9.
The subproof is completed by applying H4.
Assume H8: x0 = u10.
The subproof is completed by applying H5.
Assume H8: x0 = u11.
Apply FalseE with x1 u11.
Apply In_irref with x0.
Apply H8 with λ x2 x3 . x0 ∈ x3.
The subproof is completed by applying H6.
Let x2 of type ι → ι → ο be given.
Assume H8: x2 x0 x0.
The subproof is completed by applying H8.
■