unfolding structural recursion

Stream: general

[Satoshi Kura]

I am trying to define denotational semantics of simply typed lambda calculus using lean 3.49.1 with mathlib (commit 22feff54d70f45fe7f4dfdd7770e32e13f1aa3d4).
However, lean fails to prove an obvious equation about structural recursion at the bottom of the following code.
What do you think is the reason?

import category_theory.closed.cartesian

section

inductive Member {α : Type} : α → list α → Type
| head : ∀ {a as}, Member a (a::as)
| tail : ∀ {a b bs}, Member a bs → Member a (b::bs)

inductive Ty (β : Type)
| base : β → Ty
| fn : Ty → Ty → Ty

inductive Term {β : Type} : list (Ty β) → Ty β → Type
| var   : ∀ {ty ctx}, Member ty ctx → Term ctx ty
| app   : ∀ {ctx dom ran}, Term ctx (Ty.fn dom ran) → Term ctx dom → Term ctx ran
| lam   : ∀ {ctx dom ran}, Term (dom :: ctx) ran → Term ctx (Ty.fn dom ran)

end

section

open category_theory category_theory.category

universes v u w

variables {C : Type u} [category.{v} C] [limits.has_finite_products C] [category_theory.cartesian_closed C]

variables {β : Type} (a : β → C)

noncomputable def Ty.denote : Ty β → C
| (Ty.base b) := a b
| (Ty.fn t1 t2) := t1.denote ⟹ t2.denote

noncomputable def ctx_denote : list (Ty β) → C
| [] := limits.terminal C
| (x::xs) := limits.prod (Ty.denote a x) (ctx_denote xs)

noncomputable def term_var_proj {ty : Ty β} : Π {ctx : list (Ty β)}, Member ty ctx → (ctx_denote a ctx ⟶ Ty.denote a ty)
| _ Member.head := limits.prod.fst
| (h::tl) (Member.tail m) := begin dsimp [ctx_denote], exact limits.prod.snd end ≫ term_var_proj m

noncomputable def Term.denote : Π {ctx : list (Ty β)} {ty : Ty β}, Term ctx ty → (ctx_denote a ctx ⟶ Ty.denote a ty)
| ctx ty (Term.var m) := term_var_proj a m  --  Term.denote a (Term.var m) is defined here.
| ctx cod (Term.app m n) := limits.prod.lift n.denote m.denote ≫ begin dsimp [Ty.denote], exact ((exp.ev _).app _) end
| ctx (Ty.fn dom cod) (Term.lam m) := begin
    dsimp [Ty.denote],
    apply cartesian_closed.curry,
    have m_denote := Term.denote m,
    dsimp [ctx_denote] at m_denote,
    exact m_denote,
end

example {ctx : list (Ty β)} {ty : Ty β} (m : Member ty ctx) : Term.denote a (Term.var m) = term_var_proj a m := rfl
-- type mismatch, term
--   rfl
-- has type
--   ?m_2 = ?m_2
-- but is expected to have type
--   Term.denote a (Term.var m) = term_var_proj a m

end