induction Γ using List.induction_with_singleton with
| hnil => simp_all [List.disj'_nil, efq!];
| hsingle => simp_all [List.mem_singleton, List.disj'_singleton, imp_id!];
| hcons q Δ hΔ ih =>
  simp [List.disj'_cons_nonempty hΔ];
  simp at hd;
  have ⟨hd₁, hd₂⟩ := hd;
  subst hd₁;
  apply provable_iff_provable.mpr;
  apply deduct_iff.mpr;
  exact disj₃'! (by simp) (weakening! (by simp) $ provable_iff_provable.mp $ ih hd₂) id!
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 𝓢
hd : ∀ q ∈ Γ, q = p
⊢ 𝓢 ⊢! Γ.disj' ⟶ p
no goals