. simp_all [(List.remove_cons_of_ne Γ hpq)];
  by_cases hqΓ : Γ.remove p = [];
  . simp_all;
    exact disj₃''! disj₂! (imp_trans! ih $ or_replace_right! efq!);
  . simp [(List.disj'_cons_nonempty hqΓ)];
    exact disj₃''! (imp_trans! disj₁! disj₂!) (imp_trans! ih (or_replace_right! 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
⊢ 𝓢 ⊢! q ⋎ Γ.disj' ⟶ p ⋎ (List.remove p (q :: Γ)).disj'
no goals