begin

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

end