relabel_id

Mathlib.ModelTheory.Syntax

URI: https://scilib.ai/kg/mathlib#FirstOrder.Language.Term.relabel_id

Lean4

theorem relabel_id (t : L.Term α) : t.relabel id = t := by
  induction t with
  | var => rfl
  | func _ _ ih => simp [ih]

Похожие утверждения

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru