Proofgold Term Root Disambiguation

λ x0 . λ x1 : ι → ι → ι . λ x2 . ∀ x3 . x3 ∈ x0 ⟶ {x1 x3 (x1 x4 (explicit_Group_inverse x0 x1 x3))|x4 ∈ x2} ⊆ x2

as obj
d7a95..^{explicit_normal}

as prop
-

theory
HotG

stx
a0c68..

address
TMUp9..^{explicit_normal}