DeZero.eq_subst

Énoncé

∀ {α : Sort u} {motif : α → Prop} {a : α} {b : α} (h : a = b) (ha : motif a), motif b

Transporte une propriété le long d’une égalité : ce qui vaut pour a vaut pour b.

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

/-- Réécriture : transporte une propriété le long d'une égalité. -/
theorem eq_subst {α : Sort u} {motif : α → Prop} {a b : α} (h : a = b) (ha : motif a) : motif b :=
  Eq.rec (motive := fun x _ => motif x) ha h