Proofgold Term Root Disambiguation

λ x0 x1 . λ x2 x3 : ι → ι . λ x4 . If_i (x4 = Inj0 (Unj x4)) (x2 (Unj x4)) (x3 (Unj x4))

as obj
aa7bb..^{combine_funcs}

as prop
-

theory
HotG

stx
114a5..

address
TMKSa..^{combine_funcs}