Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Let x1 of type ι be given.
The subproof is completed by applying unknownprop_47684d77daf9976982fef9cd65f54cb0f256a9046ee087c4a3bf5f6bf45def6c with prim0 (prim1 (λ x2 . prim1 (λ x3 . prim0 (prim0 (prim0 x3 x2) (prim0 x2 x3)) (prim0 (prim0 x2 x2) (prim0 x2 x2))))) (prim0 (prim1 (λ x2 . prim1 (λ x3 . prim0 (prim0 (prim0 x3 x2) (prim0 x2 x2)) (prim0 (prim0 x3 x3) (prim0 x2 x3))))) (prim0 (prim1 (λ x2 . prim1 (λ x3 . prim0 (prim0 (prim0 x3 x2) (prim0 x2 x3)) (prim0 (prim0 x3 x2) (prim0 x3 x2))))) (prim0 (prim1 (λ x2 . prim1 (λ x3 . prim0 (prim0 (prim0 x3 x2) (prim0 x3 x2)) (prim0 (prim0 x2 x2) (prim0 x2 x2))))) (prim0 (prim1 (λ x2 . prim1 (λ x3 . prim0 (prim0 (prim0 x3 x2) (prim0 x2 x2)) (prim0 (prim0 x3 x3) (prim0 x2 x2))))) (prim0 (prim1 (λ x2 . prim1 (λ x3 . prim0 (prim0 (prim0 x3 x2) (prim0 x2 x3)) (prim0 (prim0 x2 x3) (prim0 x3 x2))))) (prim0 (prim1 (λ x2 . prim1 (λ x3 . prim0 (prim0 (prim0 x3 x2) (prim0 x2 x3)) (prim0 (prim0 x2 x2) (prim0 x3 x2))))) (prim0 (prim1 (λ x2 . prim1 (λ x3 . prim0 (prim0 (prim0 x3 x2) (prim0 x2 x2)) (prim0 (prim0 x3 x3) (prim0 x3 x3))))) (prim0 (prim1 (λ x2 . prim1 (λ x3 . prim0 (prim0 (prim0 x3 x2) (prim0 x2 x3)) (prim0 (prim0 x2 x2) (prim0 x3 x3))))) (prim0 (prim1 (λ x2 . prim1 (λ x3 . prim0 (prim0 (prim0 x3 x2) (prim0 x2 x3)) (prim0 (prim0 x2 x3) (prim0 x3 x2))))) (prim0 (prim1 (λ x2 . prim1 (λ x3 . prim0 (prim0 (prim0 x3 x2) (prim0 x2 x3)) (prim0 (prim0 x3 x3) (prim0 x2 x2))))) (prim0 (prim1 (λ x2 . prim1 (λ x3 . prim0 (prim0 (prim0 x3 x2) (prim0 x2 x3)) (prim0 (prim0 x2 x3) (prim0 x3 x2))))) (prim0 (prim1 (λ x2 . prim1 (λ x3 . prim0 (prim0 (prim0 x3 x2) ...) ...))) ...)))))))))))), ..., ....