repeat' aesop
case mp.intro.intro.bottom
g : Formula
X : Finset Formula
boxg_in_X : bottom ∈ X
projboxg_is_g :
  (match bottom with
    | □f => some f
    | x => none) =
    some g
⊢ □g ∈ X

case mp.intro.intro.atom_prop
g : Formula
X : Finset Formula
a✝ : Char
boxg_in_X : (·a✝) ∈ X
projboxg_is_g :
  (match ·a✝ with
    | □f => some f
    | x => none) =
    some g
⊢ □g ∈ X

case mp.intro.intro.neg
g : Formula
X : Finset Formula
a✝ : Formula
boxg_in_X : ~a✝ ∈ X
projboxg_is_g :
  (match ~a✝ with
    | □f => some f
    | x => none) =
    some g
⊢ □g ∈ X

case mp.intro.intro.And
g : Formula
X : Finset Formula
a✝¹ a✝ : Formula
boxg_in_X : a✝¹⋀a✝ ∈ X
projboxg_is_g :
  (match a✝¹⋀a✝ with
    | □f => some f
    | x => none) =
    some g
⊢ □g ∈ X

case mp.intro.intro.box
g : Formula
X : Finset Formula
a✝ : Formula
boxg_in_X : □a✝ ∈ X
projboxg_is_g :
  (match □a✝ with
    | □f => some f
    | x => none) =
    some g
⊢ □g ∈ X
no goals