Looks OK to me, though I can’t guarantee that there isn’t a subtle oops I haven’t spotted. (Of course it assumes you’ve got some definition for what sort of a thing (a ⇐ b) is; you might e.g. use a Kuratowski ordered pair {{a},{a,b}} or something.)
Looks OK to me, though I can’t guarantee that there isn’t a subtle oops I haven’t spotted. (Of course it assumes you’ve got some definition for what sort of a thing (a ⇐ b) is; you might e.g. use a Kuratowski ordered pair {{a},{a,b}} or something.)