Search for blocks/addresses/...
Proofgold Proof
pf
Assume H0:
∀ x0 x1 x2 .
SNoLt
0
x1
⟶
SNo
x1
⟶
SNo
x2
⟶
SNoLev
x2
∈
eps_
x0
⟶
x2
=
0
⟶
∀ x3 : ο .
x3
.
Claim L1:
SNoLt
0
1
The subproof is completed by applying SNoLt_0_1.
Claim L2:
SNo
1
The subproof is completed by applying SNo_1.
Claim L3:
SNo
0
The subproof is completed by applying SNo_0.
Claim L4:
SNoLev
0
∈
eps_
0
Apply SNoLev_0 with
λ x0 x1 .
x1
∈
eps_
0
.
Apply eps_0_1 with
λ x0 x1 .
0
∈
x1
.
The subproof is completed by applying In_0_1.
Claim L5:
not
(
0
=
0
⟶
∀ x0 : ο .
x0
)
Assume H5:
0
=
0
⟶
∀ x0 : ο .
x0
.
Apply H5.
Let x0 of type
ι
→
ι
→
ο
be given.
Assume H6:
x0
0
0
.
The subproof is completed by applying H6.
Apply L5.
Apply H0 with
0
,
1
,
0
leaving 4 subgoals.
The subproof is completed by applying L1.
The subproof is completed by applying L2.
The subproof is completed by applying L3.
The subproof is completed by applying L4.
■