case hcons.hsingle p ps hps ihp q =>
  simp_all;
  apply iff_trans! (by
    apply or_replace_right_iff!;
    simpa using @ihp [q];
  ) or_assoc!;
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
hps : ps ≠ []
ihp : ∀ {Δ : List F}, 𝓢 ⊢! (ps ++ Δ).disj' ⟷ ps.disj' ⋎ Δ.disj'
q : F
⊢ 𝓢 ⊢! (p :: ps ++ [q]).disj' ⟷ (p :: ps).disj' ⋎ [q].disj'
no goals