congrArg

Énoncé

∀ {α : Sort u} {β : Sort v} {a₁ : α} {a₂ : α} (f : α → β) (h : a₁ = a₂), f a₁ = f a₂

Applique la même fonction aux deux membres d’une égalité. C’est le bloc de la réécriture ciblée.

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.