Proofgold Proposition

∀ x0 x1 . ∀ x2 : ι → ι → ι . ∀ x3 x4 . (x4 = x3 ⟶ ∀ x5 : ο . x5) ⟶ ap (lam x1 (λ x6 . If_i (x6 = x3) x0 (x2 (ordsucc x3) x6))) x4 = ap (lam x1 (x2 (ordsucc x3))) x4

type
prop

theory
HotG

name
-

proof
PUe49..

Megalodon
-

proofgold address
TMUqJ..

creator
19014 Pr4zB../817b3..

owner
19014 Pr4zB../817b3..

term root
63c13..