begin
  (- <> @ n1 n2)
v (- @ n1 (<>p2 -> p1)) 
v (- @ n2 <>p2)
v (@ n1 p1)
end