exact iff_trans! (@ihp (q :: qs)) (by
  apply or_replace_right_iff!;
  simp [List.disj'_cons_nonempty hqs];
)
case d
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
inst✝¹ : System.NegationEquiv 𝓢
inst✝ : HasEFQ 𝓢
p : F
ps : List F
q : F
qs : List F
hps : ¬ps = []
ihp : ∀ {Δ : List F}, 𝓢 ⊢! (ps ++ Δ).disj' ⟷ ps.disj' ⋎ Δ.disj'
hqs : ¬qs = []
ihq : 𝓢 ⊢! p ⋎ (ps ++ qs).disj' ⟷ (p ⋎ ps.disj') ⋎ qs.disj'
⊢ 𝓢 ⊢! (ps ++ q :: qs).disj' ⟷ ps.disj' ⋎ q ⋎ qs.disj'
no goals