カルケドン定数つき単項述語論理なら定義できたと思う
S除去で→を削って食って手法