intro ⟨h⟩
case mp
S : Type u_1
F : Type u_2
inst✝² : LogicalConnective F
inst✝¹ : System F S
𝓢 : S
inst✝ : Minimal 𝓢
p q r : F
⊢ 𝓢 ⊢! p ⋏ q ⟶ r → 𝓢 ⊢! p ⟶ q ⟶ r
case mp
S : Type u_1
F : Type u_2
inst✝² : LogicalConnective F
inst✝¹ : System F S
𝓢 : S
inst✝ : Minimal 𝓢
p q r : F
h : 𝓢 ⊢ p ⋏ q ⟶ r
⊢ 𝓢 ⊢! p ⟶ q ⟶ r