\RequirePackage{amssymb} \let\eventually\lozenge \let\always\square \def\until{\mathop{\mathsf U}} \let\next\bigcirc \let\then\Rightarrow