exact imp_trans! distribute_multidia_and! $ by
  apply deduct'!;
  apply iff_provable_list_conj.mpr;
  intro q hq;
  simp at hq;
  cases hq with
  | inl => subst_vars; exact conj₁'! id!;
  | inr hq =>
    obtain ⟨r, hr₁, hr₂⟩ := hq;
    exact (iff_provable_list_conj.mp $ (of'! ih) ⨀ (conj₂'! $ id!)) q (by aesop);
case hcons
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 : ℕ
p : F
Γ : List F
h : ¬Γ = []
ih : 𝓢 ⊢! ◇^[n]Γ.conj' ⟶ (◇'^[n]Γ).conj'
⊢ 𝓢 ⊢! ◇^[n](p ⋏ Γ.conj') ⟶ (◇'^[n](p :: Γ)).conj'
no goals