Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Assume H0: prim1 x0 (4ae4a.. (4ae4a.. 4a7ef..)).
Apply unknownprop_dec2978c0a72cebd51fcab0a380f03d4d80d1ccd8f826d378953148c305a60f0 with 4ae4a.. 4a7ef.., x0, prim1 x0 (prim2 4a7ef.. (4ae4a.. 4a7ef..)) leaving 3 subgoals.
The subproof is completed by applying H0.
Assume H1: prim1 x0 (4ae4a.. 4a7ef..).
Claim L2: x0 = 4a7ef..
Apply unknownprop_30833a9978e304b25ffd59c347245315985872140acc9e441a97543a28184d79 with 4a7ef.., x0.
Apply unknownprop_745f0ddae55929306ce167ef9bae0ede767961c0319e8b14305a55d5b24d73e4 with x0.
The subproof is completed by applying H1.
Apply L2 with λ x1 x2 . prim1 x2 (prim2 4a7ef.. (4ae4a.. 4a7ef..)).
The subproof is completed by applying unknownprop_893870ab8a49d622c10a8fe954eea30d7bd2b94aa27e9c6b21eab85a9f81d115 with 4a7ef.., 4ae4a.. 4a7ef...
Assume H1: x0 = 4ae4a.. 4a7ef...
Apply H1 with λ x1 x2 . prim1 x2 (prim2 4a7ef.. (4ae4a.. 4a7ef..)).
The subproof is completed by applying unknownprop_70f06371245ce38fbbca963cb4d7e422ccf350d2e27735c617635b09cbcba701 with 4a7ef.., 4ae4a.. 4a7ef...
■