claim !P:(set set) prop.!Q:(set set) prop.(?f:set set.P f & Q f) -> !R:prop.(!f:set set.P f -> Q f -> R) -> R