Proofgold Term Root Disambiguation

∀ x0 x1 : ι → (ι → ο) → ο . PNoLt_pwise x0 x1 ⟶ PNoLt_pwise (PNo_downc x0) (PNo_upc x1)

as obj
-

as prop
2f244..^{PNoLt_pwise_downc_upc}

theory
HotG

stx
9543e..

address
TMaup..^{PNoLt_pwise_downc_upc}