Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Let x1 of type ι be given.
Assume H0: 2fe34.. x0 = 2fe34.. x1.
Apply unknownprop_3b55668ebff4b5090f31d28781617fd36508e9eaa3458c4a604deaa4db096497 with 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 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 ...)) ...)))))))))))), ..., ..., ....
...