Proofgold Term Root Disambiguation

∀ x0 : ι → ο . ∀ x1 : ι → ι . (∀ x2 . x0 x2 ⟶ x1 (x1 x2) = x2) ⟶ ∀ x2 . (∀ x3 . x3 ∈ x2 ⟶ x0 x3) ⟶ prim5 (prim5 x2 x1) x1 = x2

as obj
-

as prop
5faff..^{Repl_invol_eq}

theory
HotG

stx
5128f..

address
TMNjE..^{Repl_invol_eq}