Proofgold Term Root Disambiguation

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

as obj
-

as prop
393cc..^{invol_Repl_eq}

theory
HotG

stx
2cf07..

address
TMQzn..^{invol_Repl_eq}