Proofgold Term Root Disambiguation

λ x0 x1 x2 . unpack_b_o x0 (λ x3 . λ x4 : ι → ι → ι . unpack_b_o x1 (λ x5 . λ x6 : ι → ι → ι . and (x2 ∈ setexp x5 x3) (∀ x7 . x7 ∈ x3 ⟶ ∀ x8 . x8 ∈ x3 ⟶ ap x2 (x4 x7 x8) = x6 (ap x2 x7) (ap x2 x8))))

as obj
9b88c..^Hom_struct_b

as prop
-

theory
HotG

stx
820be..

address
TMVx1..^Hom_struct_b