Proofgold Proposition

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

type
prop

theory
HotG

name
-

proof
PUe49..

Megalodon
-

proofgold address
TMd6i..

creator
19014 Pr4zB../8fd29..

owner
19014 Pr4zB../8fd29..

term root
d3916..