external icsat_is_iff : prop -> bool = "icsat_is_iff"