Proofgold Term Root Disambiguation

∀ x0 : ι → ο . ∀ x1 : ι → ι → ο . wb (wrnf x0 x1) (wrex x0 x1 ⟶ wral x0 x1)

as obj
-

as prop
ce993..

theory
SetMM

stx
1f583..

address
TMMj8..