Search for blocks/addresses/...
Proofgold Proof
pf
Assume H0:
∀ x0 x1 x2 .
SNo
x0
⟶
x1
∈
x0
⟶
x2
∈
Sing
(
Sing
2
)
⟶
x2
=
Sing
2
⟶
∀ x3 : ο .
x3
.
Claim L1:
SNo
1
The subproof is completed by applying SNo_1.
Claim L2:
0
∈
1
The subproof is completed by applying In_0_1.
Claim L3:
Sing
2
∈
Sing
(
Sing
2
)
The subproof is completed by applying SingI with
Sing
2
.
Claim L4:
not
(
Sing
2
=
Sing
2
⟶
∀ x0 : ο .
x0
)
Assume H4:
Sing
2
=
Sing
2
⟶
∀ x0 : ο .
x0
.
Apply H4.
Let x0 of type
ι
→
ι
→
ο
be given.
Assume H5:
x0
(
Sing
2
)
(
Sing
2
)
.
The subproof is completed by applying H5.
Apply L4.
Apply H0 with
1
,
0
,
Sing
2
leaving 3 subgoals.
The subproof is completed by applying L1.
The subproof is completed by applying L2.
The subproof is completed by applying L3.
■