Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Let x1 of type ι be given.
Let x2 of type ι be given.
Let x3 of type ι be given.
Assume H0: cfc98.. x0 x1 = cfc98.. x2 x3.
Apply unknownprop_f4ff16b9b21fb43bec0dd0d2e94569d632f3d21b75932b9bcc0c1ffd4c0d62b6 with x0, x1, x2, x3.
Apply unknownprop_3b55668ebff4b5090f31d28781617fd36508e9eaa3458c4a604deaa4db096497 with prim0 (prim1 (λ x4 . prim1 (λ x5 . prim0 (prim0 (prim0 x5 x4) (prim0 x5 x4)) (prim0 (prim0 x5 x5) (prim0 x5 x5))))) (prim1 (λ x4 . x4)), prim0 x0 x1, prim0 (prim1 (λ x4 . prim1 (λ x5 . prim0 (prim0 (prim0 x5 x4) (prim0 x5 x4)) (prim0 (prim0 x5 x5) (prim0 x5 x5))))) (prim1 (λ x4 . x4)), prim0 x2 x3.
The subproof is completed by applying H0.