theorem Actions.persons_are_actually_agents
theorem Actions.persons_are_actually_agents
(logic_is_actual : LogicIsActual)
: ∀ (x : Type), A (Person.Is x) → A (Agent.Is x)