intro q hq
case h
F : Type u_1
inst✝⁷ : StandardModalLogicalConnective F
inst✝⁶ : DecidableEq F
S : Type u_2
inst✝⁵ : System F S
p✝ q r : F
Γ✝ Δ : List F
𝓢 : S
inst✝⁴ : Classical 𝓢
inst✝³ : System.NegationEquiv 𝓢
inst✝² : Necessitation 𝓢
inst✝¹ inst✝ : HasAxiomK 𝓢
n : ℕ
p : F
Γ : List F
h : ¬Γ = []
ih : 𝓢 ⊢! ◇^[n]Γ.conj' ⟶ (◇'^[n]Γ).conj'
⊢ ∀ p_1 ∈ ◇'^[n](p :: Γ), { ctx := [◇^[n]p ⋏ ◇^[n]Γ.conj'] } ⊢! p_1
case h
F : Type u_1
inst✝⁷ : StandardModalLogicalConnective F
inst✝⁶ : DecidableEq F
S : Type u_2
inst✝⁵ : System F S
p✝ q✝ r : F
Γ✝ Δ : List F
𝓢 : S
inst✝⁴ : Classical 𝓢
inst✝³ : System.NegationEquiv 𝓢
inst✝² : Necessitation 𝓢
inst✝¹ inst✝ : HasAxiomK 𝓢
n : ℕ
p : F
Γ : List F
h : ¬Γ = []
ih : 𝓢 ⊢! ◇^[n]Γ.conj' ⟶ (◇'^[n]Γ).conj'
q : F
hq : q ∈ ◇'^[n](p :: Γ)
⊢ { ctx := [◇^[n]p ⋏ ◇^[n]Γ.conj'] } ⊢! q