types - リーンで次のエラーを解釈する方法は?

Question

次のコードがあります。

example (x y : ℕ):
    (x + y) * (x+y ) = x*x + y*x + x*y +y*y
    :=
    have s₀:(x+y)*(x+y) = (x+y)*x + (x+y)*y, 
        from nat.left_distrib (x+y) x y ,
    have s₁: (x+y)*x = x*x + y*x,
        from nat.right_distrib x y x,
    have s₂: (x+y)*y = x*y + y*y,
        from nat.right_distrib x y y,
    have s₃: (x+y)*(x+y) = x*x + y*x + (x+y)*y, 
        from s₁ ▸ s₀, 
    show   (x + y) * (x+y ) = x*x + y*x + x*y +y*y , 
        from 
        (@eq.subst ℕ  (λ T:ℕ , (x+y)*(x+y) = x*x + y*x + T ) 
        ( (x+y)*y ) (x*y + y*y) ) (s₂)  (s₃) 

問題は最後のステップ (ショー) にあるようです。コンパイラは次のように伝えます。

term
  s₂ ▸ s₃
has type
  (λ (T : ℕ), (x + y) * (x + y) = x * x + y * x + T) (x * y + y * y)
but is expected to have type
  (x + y) * (x + y) = x * x + y * x + x * y + y * y

理解できません。どちらも同じタイプではないですか？