theorem AxiomaticThinking.observation_resolves_contradiction_in_empty_system
theorem AxiomaticThinking.observation_resolves_contradiction_in_empty_system
: ∀ (k k' : BeliefSystem) (b : Belief) (p : Prop) (o : Observation),
  ObservationsCorrespondToAProposition →
    k.val includes b.val →
      b.val belief-corresponds-to ¬p →
        o.val informs b.val → o.val contains p → k' is-empty-belief-system → ∃ b', k' resolves b' in-belief-system k