Proofgold Object

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

type
ι → ι → (ι → ι) → (ι → ι) → ι → ι

theory
HotG

name
combine_funcs

definition
PUMB7..

Megalodon
combine_funcs

proofgold address
TMJtk..^{combine_funcs}

creator
4898 Pr6Pc../a7430..

owner
4898 Pr6Pc../a7430..

term root
ccac4..