simp [h, h']
case mp.intro.intro
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
Γ : TCtxt V 𝕍
M N : Λ V 𝕍
τ σ : 𝕋 𝕍
h : typeOf Γ M = some (σ →' τ)
h' : typeOf Γ N = some σ
⊢ typeOf Γ (Λ.App M N) = some τ
no goals