Proofgold Term Root Disambiguation

λ x0 . and (struct_u x0) (unpack_u_o x0 (λ x1 . λ x2 : ι → ι . ∀ x3 . x3 ∈ x1 ⟶ x2 (x2 x3) = x2 x3))

as obj
9f253..^{struct_u_idem}

as prop
-

theory
HotG

stx
8c2f6..

address
TMFao..^{struct_u_idem}