induction Γ using List.induction_with_singleton with
| hnil => simp;
| hsingle => simp;
| hcons p Γ hΓ ih =>
  simp_all;
  constructor;
  . intro h;
    constructor;
    . exact conj₁'! h;
    . exact ih.mp (conj₂'! h);
  . rintro ⟨h₁, h₂⟩;
    exact conj₃'! h₁ (ih.mpr h₂);
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 𝓢
Γ : List F
⊢ 𝓢 ⊢! Γ.conj' ↔ ∀ p ∈ Γ, 𝓢 ⊢! p
no goals