English
For any R, l.destutter' R a is an IsChain under R.
Русский
Для любого отношения R, l.destutter' R a образует цепочку по отношению R.
LaTeX
$$$$(l.destutter'\,R\,a).IsChain\,R.$$$$
Lean4
theorem isChain_destutter' (l : List α) (a : α) : (l.destutter' R a).IsChain R := by
induction l using twoStepInduction generalizing a with
| nil => simp
| singleton => simp [apply_ite]
| cons_cons b c l IH
IH2 =>
simp_rw [destutter'_cons, apply_ite (IsChain R ·), IH, if_true_right] at IH2
simp_rw [destutter'_cons, apply_ite (IsChain R ·), apply_ite (IsChain R <| a :: ·), IH, isChain_cons_cons,
if_true_right, ite_prop_iff_and, imp_and]
exact ⟨⟨⟨swap <| fun _ => id, fun _ => IH2 c b⟩, swap <| fun _ => IH2 b a⟩, fun _ => IH2 c a⟩
