Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Assume H0: x0 ∈ setminus u15 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.
Assume H6: x1 u11.
Assume H7: x1 u12.
Assume H8: x1 u13.
Assume H9: x1 u14.
Apply setminusE with u15, u6, x0, x1 x0 leaving 2 subgoals.
The subproof is completed by applying H0.
Assume H10: x0 ∈ u15.
Assume H11: nIn x0 u6.
Apply unknownprop_694fc0de840ab2f1f5c261264c02c99f1f600514c9ad1f70a441ef6f962c2887 with x0, λ x2 . x0 = x2 ⟶ x1 x2 leaving 12 subgoals.
Apply setminusI with u16, u6, x0 leaving 2 subgoals.
Apply ordsuccI1 with u15, x0.
The subproof is completed by applying H10.
The subproof is completed by applying H11.
Assume H12: x0 = u6.
The subproof is completed by applying H1.
Assume H12: x0 = u7.
The subproof is completed by applying H2.
Assume H12: x0 = u8.
The subproof is completed by applying H3.
Assume H12: x0 = u9.
The subproof is completed by applying H4.
Assume H12: x0 = u10.
The subproof is completed by applying H5.
Assume H12: x0 = u11.
The subproof is completed by applying H6.
Assume H12: x0 = u12.
The subproof is completed by applying H7.
Assume H12: x0 = u13.
The subproof is completed by applying H8.
Assume H12: x0 = u14.
The subproof is completed by applying H9.
Assume H12: x0 = u15.
Apply FalseE with x1 u15.
Apply In_irref with x0.
Apply H12 with λ x2 x3 . x0 ∈ x3.
The subproof is completed by applying H10.
Let x2 of type ι → ι → ο be given.
Assume H12: x2 x0 x0.
The subproof is completed by applying H12.
■