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