external icsat_mk_iff : prop -> prop -> prop = "icsat_mk_iff"