append_left_iff — Mathlib

English

For every L, the step relation between L concatenated with L1 and L concatenated with L2 is equivalent to the step relation between L1 and L2.

Русский

Для произвольного L выполняется, что редукционный шаг между (L ++ L1) и (L ++ L2) эквивалентен редукционному шагу между L1 и L2.

LaTeX

$$$Step(L \!\!+\! L_1, L \!\!+\! L_2) \iff Step(L_1, L_2)$$$

Lean4

@[to_additive]
theorem append_left_iff : ∀ L, Step (L ++ L₁) (L ++ L₂) ↔ Step L₁ L₂
  | [] => by simp
  | p :: l => by simp [Step.append_left_iff l, Step.cons_cons_iff]

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