substFunc_term

Mathlib.ModelTheory.Syntax

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

Lean4

@[simp]
theorem substFunc_term (t : L.Term α) : t.substFunc Functions.term = t :=
  by
  induction t
  · rfl
  · simp only [substFunc, Functions.term, subst, ‹∀ _, _›]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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