Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Assume H0: prim1 x0 48ef8...
Let x1 of type ι be given.
Assume H1: prim1 x1 x0.
Apply unknownprop_b67f6d586fb9d8883c38540f89ba210beeb3fabc8048f066af6580d3cbff51ec with x1.
Apply unknownprop_e6223cc37d124575a1439a62a8bd81090d2105429a9944c39d898ad59aaee24d with x0, x1 leaving 2 subgoals.
Apply unknownprop_03f5f7248b8d06fe27b9a4f75f4e437d5e9b43a9092733e8b3f6dcfe61f5e308 with x0.
The subproof is completed by applying H0.
The subproof is completed by applying H1.