import PhysicsLogic.Paradigm.Dynamics

open PhysicsLogic.Paradigm.Dynamics
variable {State Time : Type}

example : ∀ d : Dynamics State Time, d.TotalDeterministicEvolution ↔
    ∀ time initial, ∃ final, d.evolves time initial final ∧
      ∀ candidate, d.evolves time initial candidate → candidate = final :=
  total_deterministic_evolution_iff_unique_successors

#print axioms total_deterministic_evolution_iff_unique_successors