Eq.trans

Énoncé

∀ {α : Sort u} {a : α} {b : α} {c : α} (h₁ : a = b) (h₂ : b = c), a = c

Enchaîne deux égalités : de a = b et b = c, tire a = c. C’est ce qu’un calc empile.

Axiomes consommés

Aucun. Cet énoncé se démontre à partir des seules règles du noyau — il ne coûte rien à qui accepte Lean.

Code

Cette déclaration vient du cœur de Lean 4 (Init.Prelude) et non de ce dépôt. Elle figure dans la bibliothèque parce que la liste blanche du projet l’autorise.