-(
   (
      <>(@c1 c2)
      &
         @ c1 (
                 ([]<>(p1 v @ c2 (p1 <-> <>p3)))
                 ->
                 (<>p1 <-> []<>(@c2 (c3 & P4)))
              )
   )

   ->

   (
      @ c2 ([]<>(p1 v @ c2 (p1 <-> <>p3)))
      ->
      @ c1 (<>p1 <-> []<>(@ c2 (c3 & P4)))
   )
)