[logic-ml] temporal type theory