theorem AxiomaticThinking.observations_dont_update_beliefs_if_person_doesnt_choose
theorem AxiomaticThinking.observations_dont_update_beliefs_if_person_doesnt_choose
(logic_is_actual : LogicIsActual)
(observations_correspond_to_prop : A ObservationsCorrespondToAProposition)
: ∀ (per : Person) (k : BeliefSystem) (b : Belief),
  A (k.val includes b.val) →
    ∀ (p : Prop),
      A (b.val corresponds-to ¬p) →
        ∀ (o : Observation),
          A (o.val informs b.val) →
            A (o.val contains p) →
              ∀ (k' : BeliefSystem),
                A (k' is-empty-belief-system ) →
                  ¬per updates-belief-system-to k' →
                    A (∃ b', k' resolves b' in-belief-system k) ∧ ¬A (per.val adopts k'.val)