 To be clear: in the language \eqref{EAL}, the precondition \(\pre^A(e)\) of an action model A may be a formula that includes an action model modality \([A',e']\) for some other action \((A',e')\in\AM_*\). For full technical details on how this works, please see  Appendix H.  