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_5ef6db00f3c15a86c1e221d4a4c3ce606c4d873a1f90dd0b36114bf603c362c9 with
abelian_Group_alt
.
The subproof is completed by applying L0.
■