Proofgold Proposition

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

type
prop

theory
HotG

name
-

proof
PUStC..

Megalodon
-

proofgold address
TMNnP..

creator
35044 PrHS6../b9f21..

owner
35044 PrHS6../b9f21..

term root
e4081..