theorem model2.statements_are_compatible
theorem model2.statements_are_compatible
: ∃ raining : Location → Prop,
        raining Location.samsHouse ∧
        ¬ raining Location.friendsHouse