match x with
  | none => simp at h
  | some val => 
    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''⟩
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 : σ)
no goals