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