theorem Actions.achieved_implies_achievable
theorem Actions.achieved_implies_achievable
(feasibility : DoingImpliesFeasible)
: ∀ {agent : Agent} {o : Outcome} {s : State} {t : Time},
  OutcomeAchievedByAgent agent o s t → OutcomeAchievableForAgent agent o s t