begin
  !(([R1](P1 --> P2)) --> (([R1] P1) --> ([R1] P2)))
end