test17.frm

begin
!(n1:(n1 & n2:(n2 & ([](p1 -->((!(p1 -> (p2 --> p1))) v p2)) --> ([]p1 --> []p2)))))
end