external icsat_mk_implies : prop -> prop -> prop = "icsat_mk_implies"