match val with
| .To σ τ' => 
  use σ
  simp only at h 
  split_ifs at h with h''
  simp only [Option.some.injEq] at h 
  rw [h] at h'
  exact ⟨h', h''⟩
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
Γ : TCtxt V 𝕍
M N : Λ V 𝕍
τ : 𝕋 𝕍
x : Option (𝕋 𝕍)
val : 𝕋 𝕍
h :
  (match some val with
    | some (τ →' σ) => if typeOf Γ N = some τ then some σ else none
    | x => none) =
    some τ
h' : typeOf Γ M = some val
⊢ ∃ σ, (Γ ⊢ M : σ →' τ) ∧ (Γ ⊢ N : σ)
no goals