p U (q /\ [] r)
p U (q /\ X(r U s))
p U (q /\ X(r /\ (<>(s /\ X(<> (t /\ X(<> (u /\ X <> v))))))))
<> (p /\ X [] q)
<> (p /\ X(q /\ X(<> r)))
<> (q /\ X(p U r))
(<> [] q) \/ (<> [] p)
[](p -> (q U r))
<>(p /\ X <>(q /\ X <>(r /\ X <> s)))
[]<>p /\ []<>q /\ []<>r /\ []<>s /\ []<>t
((p U q) U r) \/ ((q U r) U p) \/ ((r U p) U q)
[](p --> (q U ([]r \/ []s)))