Proofgold Term Root Disambiguation

∀ x0 x1 . nat_p x0 ⟶ nat_p x1 ⟶ x0 ⊆ x1 ⟶ mul_nat x0 x0 ⊆ mul_nat x1 x1

as obj
-

as prop
ad387..

theory
HotG

stx
afc5a..

address
TMLi8..