external icsat_mk_ite : prop -> prop -> prop -> prop = "icsat_mk_ite"