by_cases hqΓ : Γ.remove p = []
case neg
F : Type u_1
inst✝⁵ : LogicalConnective F
inst✝⁴ : DecidableEq F
S : Type u_2
inst✝³ : System F S
𝓢 : S
inst✝² : Minimal 𝓢
p q✝ r : F
Γ✝ Δ : List F
inst✝¹ : System.NegationEquiv 𝓢
inst✝ : HasEFQ 𝓢
q : F
Γ : List F
h : ¬Γ = []
ih : 𝓢 ⊢! Γ.disj' ⟶ p ⋎ (List.remove p Γ).disj'
hpq : ¬q = p
⊢ 𝓢 ⊢! q ⋎ Γ.disj' ⟶ p ⋎ (q :: List.remove p Γ).disj'
case pos
F : Type u_1
inst✝⁵ : LogicalConnective F
inst✝⁴ : DecidableEq F
S : Type u_2
inst✝³ : System F S
𝓢 : S
inst✝² : Minimal 𝓢
p q✝ r : F
Γ✝ Δ : List F
inst✝¹ : System.NegationEquiv 𝓢
inst✝ : HasEFQ 𝓢
q : F
Γ : List F
h : ¬Γ = []
ih : 𝓢 ⊢! Γ.disj' ⟶ p ⋎ (List.remove p Γ).disj'
hpq : ¬q = p
hqΓ : List.remove p Γ = []
⊢ 𝓢 ⊢! q ⋎ Γ.disj' ⟶ p ⋎ (q :: List.remove p Γ).disj'

case neg
F : Type u_1
inst✝⁵ : LogicalConnective F
inst✝⁴ : DecidableEq F
S : Type u_2
inst✝³ : System F S
𝓢 : S
inst✝² : Minimal 𝓢
p q✝ r : F
Γ✝ Δ : List F
inst✝¹ : System.NegationEquiv 𝓢
inst✝ : HasEFQ 𝓢
q : F
Γ : List F
h : ¬Γ = []
ih : 𝓢 ⊢! Γ.disj' ⟶ p ⋎ (List.remove p Γ).disj'
hpq : ¬q = p
hqΓ : ¬List.remove p Γ = []
⊢ 𝓢 ⊢! q ⋎ Γ.disj' ⟶ p ⋎ (q :: List.remove p Γ).disj'