- couple->tuple cplprocedure
function (result)
(couple->tuple cpl) requires (%couple? cpl) ensures (and (%tuple? result) (= (%tuple-length result) 2))
function (result)
(couple->tuple cpl) requires (%couple? cpl) ensures (and (%tuple? result) (= (%tuple-length result) 2))