Search for blocks/addresses/...
Proofgold Proof
pf
Claim L0:
∀ x0 .
abelian_Group_alt
x0
⟶
struct_b
x0
Let x0 of type
ι
be given.
Assume H0:
abelian_Group_alt
x0
.
Apply H0 with
struct_b
x0
.
Assume H1:
struct_b
x0
.
Assume H2:
unpack_b_o
x0
(
λ x1 .
λ x2 :
ι →
ι → ι
.
and
(
explicit_Group
x1
x2
)
(
explicit_abelian
x1
x2
)
)
.
The subproof is completed by applying H1.
Apply unknownprop_be2503b86c1e5792746c6adc58383e3972a7c1b0d953c88e847e4de130b06873 with
abelian_Group_alt
.
The subproof is completed by applying L0.
■