rw [h'] at h
case mpr
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
Γ : TCtxt V 𝕍
M N : Λ V 𝕍
τ : 𝕋 𝕍
h :
  (match typeOf Γ M with
    | some (τ →' σ) => if typeOf Γ N = some τ then some σ else none
    | x => none) =
    some τ
x : Option (𝕋 𝕍)
h' : typeOf Γ M = x
⊢ ∃ σ, (Γ ⊢ M : σ →' τ) ∧ (Γ ⊢ N : σ)
case mpr
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
Γ : TCtxt V 𝕍
M N : Λ V 𝕍
τ : 𝕋 𝕍
x : Option (𝕋 𝕍)
h :
  (match x with
    | some (τ →' σ) => if typeOf Γ N = some τ then some σ else none
    | x => none) =
    some τ
h' : typeOf Γ M = x
⊢ ∃ σ, (Γ ⊢ M : σ →' τ) ∧ (Γ ⊢ N : σ)