Search for blocks/addresses/...
Proofgold Proof
pf
Apply set_ext with
real
,
{x0 ∈
e523d..
|
28f8d..
x0
=
x0
}
leaving 2 subgoals.
Let x0 of type
ι
be given.
Assume H0:
x0
∈
real
.
Apply SepI with
e523d..
,
λ x1 .
28f8d..
x1
=
x1
,
x0
leaving 2 subgoals.
Apply unknownprop_b8e2f6014b0a1d8ddf617d3b0c26c00e0775cc15081d13f5b0fb7d075511e309 with
x0
.
The subproof is completed by applying H0.
Apply unknownprop_043a3a62e09a1e356d458c560264602babef6a620fa61db7abeb4595eeb25ec6 with
x0
.
The subproof is completed by applying H0.
Let x0 of type
ι
be given.
Assume H0:
x0
∈
{x1 ∈
e523d..
|
28f8d..
x1
=
x1
}
.
Apply SepE with
e523d..
,
λ x1 .
28f8d..
x1
=
x1
,
x0
,
x0
∈
real
leaving 2 subgoals.
The subproof is completed by applying H0.
Assume H1:
x0
∈
e523d..
.
Assume H2:
28f8d..
x0
=
x0
.
Apply H2 with
λ x1 x2 .
x1
∈
real
.
Apply unknownprop_bf35ed077052d180738002d3131b9c960f2105b6fc771a9376424dc88c5accaa with
x0
.
The subproof is completed by applying H1.
■