Proofgold Term Root Disambiguation

∀ x0 . nat_p x0 ⟶ ∀ x1 . nat_p x1 ⟶ x0 ⊆ x1 ⟶ ∀ x2 : ο . (∀ x3 . and (nat_p x3) (x1 = add_nat x3 x0) ⟶ x2) ⟶ x2

as obj
-

as prop
2c7fa..^{nat_Subq_add_ex}

theory
HotG

stx
87341..

address
TMYx5..^{nat_Subq_add_ex}