Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Let x1 of type ιιι be given.
Assume H0: explicit_Group x0 x1.
Apply explicit_Group_identity_prop with x0, x1, prim1 (explicit_Group_identity x0 x1) x0 leaving 2 subgoals.
The subproof is completed by applying H0.
Assume H1: prim1 (explicit_Group_identity x0 x1) x0.
Assume H2: and (∀ x2 . prim1 x2 x0and (x1 (explicit_Group_identity x0 x1) x2 = x2) (x1 x2 (explicit_Group_identity x0 x1) = x2)) (∀ x2 . prim1 x2 x0∃ x3 . and (prim1 x3 x0) (and (x1 x2 x3 = explicit_Group_identity x0 x1) (x1 x3 x2 = explicit_Group_identity x0 x1))).
The subproof is completed by applying H1.