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

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
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