induction Γ with
| nil =>
  simp [andImplyIffImplyImply'!];
  constructor;
  . intro h; apply imp_swap'!; exact dhyp! h;
  . intro h; exact imp_swap'! h ⨀ verum!;
| cons q ih => simp;
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 𝓢
⊢ 𝓢 ⊢! (p :: Γ).conj' ⟶ q ↔ 𝓢 ⊢! p ⋏ Γ.conj' ⟶ q
no goals