external icsat_mk_not : prop -> prop = "icsat_mk_not"