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