begin
 ( 
   (@ n1 n2 & @ n1 ((p2 v @ n2 p1) -> p3))
    & 
   - (@ n2 (p2 v @ n2 p1) -> @n1 p3)
  )

end