Leanと様相論理