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