constructor
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
⊢ (∃ a ∈ X,
      (match a with
        | □f => some f
        | x => none) =
        some g) →
    □g ∈ X

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