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