Search for blocks/addresses/...
Proofgold Proof
pf
Let x0 of type
ι
be given.
Apply GroupI with
{x1 ∈
setexp
x0
x0
|
bij
x0
x0
(
λ x2 .
ap
x1
x2
)
}
,
λ x1 x2 .
lam
x0
(
λ x3 .
ap
x2
(
ap
x1
x3
)
)
.
The subproof is completed by applying explicit_Group_symgroup with
x0
.
■