Proofgold Term Root Disambiguation

λ x0 . and (struct_r x0) (unpack_r_o x0 (λ x1 . λ x2 : ι → ι → ο . and (∀ x3 . x3 ∈ x1 ⟶ not (x2 x3 x3)) (∀ x3 . x3 ∈ x1 ⟶ ∀ x4 . x4 ∈ x1 ⟶ ∀ x5 . x5 ∈ x1 ⟶ x2 x3 x4 ⟶ x2 x4 x5 ⟶ x2 x3 x5)))

as obj
adb47..^{struct_r_partialord}

as prop
-

theory
HotG

stx
21a1b..

address
TMYDE..^{struct_r_partialord}