theorem Actions.an_agents_outcome_may_require_two_steps
theorem Actions.an_agents_outcome_may_require_two_steps
: ∀ (agent : Agent) (o : Outcome) (s0 s1 : State) (t0 t1 : Time) (a0 a1 : Action) (p0 p1 : Predisposition),
  agent.val predisposed-toward p0.val →
    p0.val is-manifested-by a0.val →
      a0.val action-is-feasible-for-agent agent.val in-state s0.val →
        Elapses t0 s0 a0 t1 s1 →
          agent.val predisposed-toward p1.val →
            p1.val is-manifested-by a1.val →
              a1.val action-is-feasible-for-agent agent.val in-state s1.val →
                a1.val results-in o.val →
                  (∀ (a : Action),
                      a.val action-is-feasible-for-agent agent.val in-state s0.val → ¬a.val results-in o.val) →
                    OutcomeAchievableForAgent agent o s0 t0 ∧
                      ¬∃ a, a.val action-is-feasible-for-agent agent.val in-state s0.val ∧ a.val results-in o.val