rw [h, Option.some.injEq] at h'
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
Γ : TCtxt V 𝕍
M : Λ V 𝕍
σ τ : 𝕋 𝕍
h : typeOf Γ M = some σ
h' : typeOf Γ M = some τ
⊢ σ = τ
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
Γ : TCtxt V 𝕍
M : Λ V 𝕍
σ τ : 𝕋 𝕍
h : typeOf Γ M = some σ
h' : σ = τ
⊢ σ = τ