begin
-(
   (
      <>(@n1 n2)
      &
         @ n1 (
                 ([]<>(p1 v @ n2 (p1 <--> <>p3)))
                 ->
                 (<>p1 <--> []<>(@n2 (n3 & P4)))
              )
   )

   ->

   (
      @ n2 ([]<>(p1 v @ n2 (p1 <--> <>p3)))
      ->
      @ n1 (<>p1 <--> []<>(@ n2 (n3 & P4)))
   )
)

end