induction Γ using List.induction_with_singleton with
| hnil => simp;
| hsingle => simp;
| hcons p Γ h ih =>
  simp_all;
  constructor;
  . intro h;
    have := distribute_multibox_and'! h;
    constructor;
    . exact conj₁'! this;
    . exact ih.mp (conj₂'! this);
  . rintro ⟨h₁, h₂⟩;
    exact collect_multibox_and'! $ conj₃'! h₁ (ih.mpr h₂);
F : Type u_1
inst✝⁷ : StandardModalLogicalConnective F
inst✝⁶ : DecidableEq F
S : Type u_2
inst✝⁵ : System F S
p q r : F
Γ Δ : List F
𝓢 : S
inst✝⁴ : Classical 𝓢
inst✝³ : System.NegationEquiv 𝓢
inst✝² : Necessitation 𝓢
inst✝¹ inst✝ : HasAxiomK 𝓢
n : ℕ
⊢ 𝓢 ⊢! □^[n]Γ.conj' ↔ ∀ p ∈ Γ, 𝓢 ⊢! □^[n]p
no goals