import PhysicsLogic.Philosophy.ProbabilityRoles

open PhysicsLogic.Philosophy.ProbabilityRoles
variable {S P M : Type}

example : ∀ (c : TypicalitySelectionContext S P M), c.TypicalPropertyBridge ↔
    ∀ m s, c.typical m s → ∀ p, c.propertyTypicalFor m p → c.hasProperty s p :=
  typical_property_bridge_iff_selected_state_soundness

example : ∀ (c : TypicalitySelectionContext S P M) (m : M),
    c.TypicalPropertyBridge → c.TypicalStateScopeInhabitedFor m →
      ∃ s, c.typical m s ∧ ∀ p, c.propertyTypicalFor m p → c.hasProperty s p :=
  sound_nonempty_selection_has_simultaneous_properties

#print axioms typical_property_bridge_iff_selected_state_soundness
#print axioms sound_nonempty_selection_has_simultaneous_properties