rintro ⟨hpq⟩ ⟨hp⟩
S : Type u_1
F : Type u_2
inst✝² : LogicalConnective F
inst✝¹ : System F S
𝓢 : S
p q : F
inst✝ : ModusPonens 𝓢
⊢ 𝓢 ⊢! p ⟶ q → 𝓢 ⊢! p → 𝓢 ⊢! q
case intro.intro
S : Type u_1
F : Type u_2
inst✝² : LogicalConnective F
inst✝¹ : System F S
𝓢 : S
p q : F
inst✝ : ModusPonens 𝓢
hpq : 𝓢 ⊢ p ⟶ q
hp : 𝓢 ⊢ p
⊢ 𝓢 ⊢! q