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