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
```