intro rhs
case mpr
g : Formula
X : Finset Formula
⊢ □g ∈ X →
    ∃ a ∈ X,
      (match a with
        | □f => some f
        | x => none) =
        some g
case mpr
g : Formula
X : Finset Formula
rhs : □g ∈ X
⊢ ∃ a ∈ X,
    (match a with
      | □f => some f
      | x => none) =
      some g