§ Subject reduction in Lean

Not exactly. Subject reduction is the property that if you replace a subterm of a term with a defeq one (especially if the subterm is the result of reduction), the resulting big term remains typecheckable. This fails in lean because if you reduce some of the identities in @id A (@id B (@id C t)) you can deduce transitivity of defeq, so by applying one of the counterexamples to transitivity you get a term such that reducing the internal identity functions results in another term that doesn't typecheck 
variables {A : Type} {R : A → A → Prop} (x : A) (h : acc R x)

def my_rec : ∀ x : A, acc R x → ℕ := @acc.rec A R (λ _, ℕ) (λ _ _ _, 1)
def inv {x : A} (h : acc R x) : acc R x := acc.intro x (λ y h', acc.inv h h')
example : inv h = h := rfl -- ok
#reduce my_rec x (inv h) -- 1
#reduce my_rec x h -- acc.rec _ h

-- failure of transitivity
#check (rfl : my_rec x (inv h) = 1) -- ok
#check (rfl : inv h = h) -- ok
#check (rfl : my_rec x (inv h) = my_rec x h) -- ok
#check (rfl : my_rec x h = 1) -- fail

-- failure of SR:
#check @id (my_rec x h = 1) (@id (my_rec x (inv h) = 1) rfl) -- ok
#check @id (my_rec x h = 1) (@id (1 = 1) rfl) -- fail

-- fooling tactics into producing type incorrect terms:
def T (X : 1 = my_rec x h → Type) :
  X (@id (1 = my_rec x (inv h)) rfl) = X (@id (1 = my_rec x (inv h)) rfl) :=
by { dsimp, refl }
-- kernel failed to type check declaration 'T' this is usually due to a buggy tactic or a bug in the builtin elaborator
-- elaborated type:
--   ∀ {A : Type} {R : A → A → Prop} (x : A) (h : acc R x) (X : 1 = my_rec x h → Type), X _ = X _
-- elaborated value:
--   λ {A : Type} {R : A → A → Prop} (x : A) (h : acc R x) (X : 1 = my_rec x h → Type), id (eq.refl (X rfl))
-- nested exception message:
-- type mismatch at application
--   X rfl
-- term
--   rfl
-- has type
--   1 = 1
-- but is expected to have type
--   1 = my_rec x h