. apply FiniteContext.deduct'!;
  have hp : [p ⋏ (q ⋏ r)] ⊢[𝓢]! p := conj₁'! id!;
  have hq : [p ⋏ (q ⋏ r)] ⊢[𝓢]! q := conj₁'! $ conj₂'! id!;
  have hr : [p ⋏ (q ⋏ r)] ⊢[𝓢]! r := conj₂'! $ conj₂'! id!;
  apply conj₃'!;
  . exact conj₃'! hp hq;
  . exact hr;
case 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 𝓢
⊢ 𝓢 ⊢! p ⋏ q ⋏ r ⟶ (p ⋏ q) ⋏ r
no goals