Change Inhabited to Nonempty in ForcingRelation

[Copilot]

The falsum lemmas in ForcingRelation.AllForces and WeakForcingRelation.AllForces used [Inhabited W] as their world non-emptiness constraint, while the rest of the Kripke semantics uniformly uses [Nonempty W].

Changes

• ForcingRelation.AllForces.falsum: [Inhabited W] → [Nonempty W]
• WeakForcingRelation.AllForces.falsum: [Inhabited ℙ] → [Nonempty ℙ]
• Proof terms updated from h default to h (Classical.choice inferInstance) since Nonempty does not expose a default element

-- Before
@[simp] lemma falsum [BasicSemantics W] [Inhabited W] : ¬W ∀⊩ ⊥ := fun h ↦ by simpa using h default

-- After
@[simp] lemma falsum [BasicSemantics W] [Nonempty W] : ¬W ∀⊩ ⊥ := fun h ↦ by simpa using h (Classical.choice inferInstance)

Original prompt

---

This section details on the original issue you should resolve

<issue_title>Change Inhabited to Nonempty in ForcingRelation</issue_title>
<issue_description>> ForcingRelation.AllForces.falsum の仮定が Nonempty ではなく Inhabited なのは何かしら意図があるのだろうか？現状のKripke意味論のWorldの仮定はNonemptyにしているので微妙に合ってない（といっても1行ぐらいの差だが）

とくに意図はなかった．Nonempty に変えるべきだと思う．

Originally posted by @iehality in #790 (comment)
</issue_description>

Comments on the Issue (you are @copilot in this section)

• Fixes Change Inhabited to Nonempty in ForcingRelation #795

---

✨ Let Copilot coding agent set things up for you — coding agent works faster and does higher quality work when set up for your repo.