Example of non-transitivity of definitional equality in Lean involving the computation rule for `well_founded.fix_F`.

wf_fix_F_non_trans.lean

variables {α : Sort*} {r : α → α → Prop} {C : α → Sort*} (x : α) (acx : acc r x)
variable F : Π x, (Π y, r y x → C y) → C x

namespace well_founded

lemma fix_F_eq0 : fix_F F x acx = fix_F F x (acc.intro x $ λ y, acx.inv) := rfl
lemma fix_F_eq1 : fix_F F x (acc.intro x $ λ y, acx.inv) = F x (λ y p, fix_F F y $ acx.inv p) := rfl
lemma fix_F_eq2 : fix_F F x acx = F x (λ y p, fix_F F y $ acx.inv p) := rfl
/- fix_F_eq2 fails but fix_F_eq0 and fix_F_eq1 work, demonstrating nontransitivity. -/

lemma fix_F_eq2' : fix_F F x acx = F x (λ y p, fix_F F y $ acx.inv p) :=
by { change fix_F F x (acc.intro x $ λ y, acx.inv) = _, refl } /- works -/
#print fix_F_eq2' /- id (eq.refl (fix_F F x (acc.intro x (λ (y : α), acx.inv)))) -/
/- The original proof: acc.drec (λ x r ih, rfl) acx -/
/- by { dsimp only [← acc.intro_inv], refl } doesn't work, where
  lemma acc.intro_inv (x : α) (acx : acc r x) : acc.intro x (λ y, acx.inv) = acx := rfl -/

lemma fix_F_eq2'' : fix_F F x acx = F x (λ y p, fix_F F y $ acx.inv p) :=
eq.refl (fix_F F x (acc.intro x (λ (y : α), acx.inv))) /- also works! -/

end well_founded