import Axiom
import A.ta3nj1a4
import A.r59jf3ak

open scoped r59jf3ak
open ta3nj1a4

namespace j8f0q7re

namespace model1

  def P : Prop := "it's raining today"

  def SamStatement    := P
  def FriendStatement := ¬ P

  theorem statements_are_contradictory
      (sam_statement : SamStatement)
      (friend_statement : FriendStatement)
    : False := by contradiction

end model1

namespace model2

  inductive Location where
  | samsHouse
  | friendsHouse

  def P : Location → Prop := "it's raining today"
  
  def SamStatement    := P Location.samsHouse
  def FriendStatement := ¬ P Location.friendsHouse

  theorem statements_are_compatible :
      ∃ raining : Location → Prop,
        raining Location.samsHouse ∧
        ¬ raining Location.friendsHouse := by
    exact ⟨fun | .samsHouse => True | .friendsHouse => False,
      True.intro, id⟩

end model2

end j8f0q7re