split_ifs at h with h''
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
Γ : TCtxt V 𝕍
M N : Λ V 𝕍
τ : 𝕋 𝕍
x : Option (𝕋 𝕍)
val σ τ' : 𝕋 𝕍
h : (if typeOf Γ N = some σ then some τ' else none) = some τ
h' : typeOf Γ M = some (σ →' τ')
⊢ (Γ ⊢ M : σ →' τ) ∧ (Γ ⊢ N : σ)
case inl
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
Γ : TCtxt V 𝕍
M N : Λ V 𝕍
τ : 𝕋 𝕍
x : Option (𝕋 𝕍)
val σ τ' : 𝕋 𝕍
h' : typeOf Γ M = some (σ →' τ')
h'' : typeOf Γ N = some σ
h : some τ' = some τ
⊢ (Γ ⊢ M : σ →' τ) ∧ (Γ ⊢ N : σ)