Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Assume H0: x0 ∈ int_alt1.
Let x1 of type ο be given.
Assume H1: x0 = 0 ⟶ x1.
Assume H2: x0 ∈ setminus omega 1 ⟶ x1.
Assume H3: ∀ x2 . x2 ∈ setminus omega 1 ⟶ x0 = minus_SNo x2 ⟶ x1.
Claim L4: ∀ x2 . x2 ∈ setminus omega 1 ⟶ x0 = x2 ⟶ x1
Let x2 of type ι be given.
Assume H4: x2 ∈ setminus omega 1.
Assume H5: x0 = x2.
Apply H2.
Apply H5 with λ x3 x4 . x4 ∈ setminus omega 1.
The subproof is completed by applying H4.
Apply unknownprop_28d247415f1c7ed197c5b3921d407caa1ec338b02ea0677564d53f2a37c403d7 with λ x2 . x0 = x2 ⟶ x1, x0 leaving 5 subgoals.
The subproof is completed by applying H1.
The subproof is completed by applying L4.
The subproof is completed by applying H3.
The subproof is completed by applying H0.
Let x2 of type ι → ι → ο be given.
Assume H5: x2 x0 x0.
The subproof is completed by applying H5.
■