English
The reduction of p :: L1 to p :: L2 is equivalent to the reduction of L1 to L2.
Русский
Редукция p :: L1 к p :: L2 эквивалентна редукции L1 к L2.
LaTeX
$$$Red(p :: L_1, p :: L_2) \leftrightarrow Red(L_1, L_2)$$$
Lean4
@[to_additive]
theorem cons_cons_iff (p) : Red (p :: L₁) (p :: L₂) ↔ Red L₁ L₂ :=
Iff.intro
(by
generalize eq₁ : (p :: L₁ : List _) = LL₁
generalize eq₂ : (p :: L₂ : List _) = LL₂
intro h
induction h using Relation.ReflTransGen.head_induction_on generalizing L₁ L₂ with
| refl =>
subst_vars
cases eq₂
constructor
| head h₁₂ h ih =>
subst_vars
obtain ⟨a, b⟩ := p
rw [Step.cons_left_iff] at h₁₂
rcases h₁₂ with (⟨L, h₁₂, rfl⟩ | rfl)
· exact (ih rfl rfl).head h₁₂
· exact (cons_cons h).tail Step.cons_not_rev)
cons_cons
