cons_not — Mathlib

English

Prepending (x, b) and then (x, ¬b) yields a one-step reduction to the original tail.

Русский

Добавление слева пары (x,b) и затем (x,¬b) приводит к редукции на один шаг к исходному хвосту.

LaTeX

$$$ \\mathrm{Red}.\\mathrm{Step}\\bigl((x,b) :: (x, \\lnot b) :: L\\bigr)\\; L$$$

Lean4

@[to_additive (attr := simp)]
theorem cons_not {x b} : Red.Step ((x, b) :: (x, !b) :: L) L :=
  @Step.not _ [] _ _ _

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