S130    ~@xPx -||- $x~Px       S131    ~$xPx -||- @x~Px       S132    ~@x~Px -||- $xPx       S133    ~$x~Px -||- @xPx       S134    @x(Px & Qx) -||- @xPx & @xQx       S135    @x(Px -> Q) -||- $xPx -> Q       S136    @xPx v @xQx |- @x(Px v Qx)       S137    $xy(Px & Qy) -||- $xPx & $xQx       S138    $x(Px v Qx) -||- $xPx v $xQx       S139    $x(Px -> Q) -||- @xPx -> Q       S140    P -> $xQx -||- $x(P -> Qx)       S141    P -> @xQx -||- @x(P -> Qx)