external icsat_mk_or : prop list -> prop = "icsat_mk_or"