induction Γ using List.induction_with_singleton with
| hnil => simp;
| hsingle q =>
  simp;
  by_cases h: q = p;
  . subst_vars; simp;
  . simp [(List.remove_singleton_of_ne h)];
| hcons q Γ h ih =>
  simp [(List.disj'_cons_nonempty h)];
  by_cases hpq : q = p;
  . simp_all only [ne_eq, List.remove_cons_self]; exact disj₃''! disj₁! ih;
  . 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₂!));
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 𝓢
⊢ 𝓢 ⊢! Γ.disj' ⟶ p ⋎ (List.remove p Γ).disj'
no goals