Why is $AF \phi \lor \varphi$ not equivalent to $AF \phi \lor AF \varphi$?
You also need to argue the other way around. &quot;Each path has either $\psi$ or $\varphi$&quot; is not the same as &quot;either each path has $\psi$ or each path has $\varphi$&quot;.