cons_cons_iff — Mathlib

English

Let α be a type and L1, L2 be lists of pairs with elements in α × Bool. For any fixed p, the reduction step relating p :: L1 to p :: L2 holds if and only if the reduction step relating L1 to L2 holds.

Русский

Пусть α — множество, L1 и L2 — списки пар из α × Bool. Для любого фиксированного p выполняется: шаг редукции между p :: L1 и p :: L2 эквивалентен шагу редукции между L1 и L2.

LaTeX

$$$Step(p :: L_1, p :: L_2) \leftrightarrow Step(L_1, L_2)$$$

Lean4

@[to_additive]
theorem cons_cons_iff : ∀ {p : α × Bool}, Step (p :: L₁) (p :: L₂) ↔ Step L₁ L₂ := by
  simp +contextual [Step.cons_left_iff, iff_def, or_imp]

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