[STATEMENT]
lemma box_omega_unfold_n:
  "|x\<^sup>\<omega> \<squnion> x\<^sup>\<star>]n(y) = n(y) * |n(y) * x]|x\<^sup>\<omega> \<squnion> x\<^sup>\<star>]n(y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. | x\<^sup>\<omega> \<squnion> x\<^sup>\<star> ] n y = n y * | n y * x ] | x\<^sup>\<omega> \<squnion> x\<^sup>\<star> ] n y
[PROOF STEP]
by (smt an_export an_n_L box_diamond diamond_box diamond_omega_unfold_an n_an_def n_export)