rcases lhs with ⟨boxg, boxg_in_X, projboxg_is_g⟩
case mp
g : Formula
X : Finset Formula
lhs :
  ∃ a ∈ X,
    (match a with
      | □f => some f
      | x => none) =
      some g
⊢ □g ∈ X
case mp.intro.intro
g : Formula
X : Finset Formula
boxg : Formula
boxg_in_X : boxg ∈ X
projboxg_is_g :
  (match boxg with
    | □f => some f
    | x => none) =
    some g
⊢ □g ∈ X