theorem AxiomaticThinking.observation_can_surface_contradiction
theorem AxiomaticThinking.observation_can_surface_contradiction
(observations_correspond_to_prop : ObservationsCorrespondToAProposition)
: ∀ (b : Belief) (p : Prop),
  b.val belief-corresponds-to ¬p →
    ∀ (o : Observation),
      o.val informs b.val → o.val contains p → b.val belief-corresponds-to p ∧ b.val belief-corresponds-to ¬p