Proofgold Term Root Disambiguation

SNo_rec_i (λ x0 . λ x1 : ι → ι . SNoCut (prim5 (SNoR x0) x1) (prim5 (SNoL x0) x1))

as obj
8a6d8..^minus_SNo

as prop
-

theory
HotG

stx
2cf07..

address
TMcxv..^minus_SNo