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