Proofgold Term Root Disambiguation

∀ x0 . nat_p x0 ⟶ ∀ x1 : ι → ο . x1 0 ⟶ (∀ x2 . nat_p x2 ⟶ x0 = ordsucc x2 ⟶ x1 (ordsucc x2)) ⟶ x1 x0

as obj
-

as prop
5f4e5..^{nat_inv_impred}

theory
HF

stx
b2d3f..

address
TMZ9E..^{nat_inv_impred}