Proofgold Proposition

∀ x0 x1 . nat_p x1 ⟶ 1319b.. x1 (λ x3 . lam 2 (λ x4 . If_i (x4 = 0) (ordsucc (ap x3 0)) (ap x3 1))) (lam 2 (λ x3 . If_i (x3 = 0) 0 x0)) = lam 2 (λ x3 . If_i (x3 = 0) x1 x0)

type
prop

theory
HotG

name
-

proof
PUStC..

Megalodon
-

proofgold address
TMVHJ..

creator
35044 PrHS6../d8a13..

owner
35044 PrHS6../d8a13..

term root
34663..