cons_cons — Mathlib

English

If a list reduces to another, then prepending the same element preserves the reduction relation.

Русский

Если список редуцируется к другому, то добавление одинакового элемента в начало сохраняет редукцию.

LaTeX

$$$\forall p\; Red L_1 L_2 \Rightarrow Red (p :: L_1) (p :: L_2)$$$

Lean4

@[to_additive]
theorem cons_cons {p} : Red L₁ L₂ → Red (p :: L₁) (p :: L₂) :=
  ReflTransGen.lift (List.cons p) fun _ _ => Step.cons

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