apply impE _ h2
H : Type ?u.36701
inst✝ : HeytingAlgebra H
v : Variable → H
A B : Formula
Γ Δ : Set Formula
h1 : Provable (A ⇒ B)
h2 : Γ ⊢ A
⊢ Γ ⊢ B
H : Type ?u.36701
inst✝ : HeytingAlgebra H
v : Variable → H
A B : Formula
Γ Δ : Set Formula
h1 : Provable (A ⇒ B)
h2 : Γ ⊢ A
⊢ Γ ⊢ A ⇒ B