proposition: Lemma step_spec (rs : Ssts) a b a' b' i v : In ((a, b), (a', b')) rs -> nth_error v i = Some a -> nth_error v (S i) = Some b -> step rs v (map (fun j => if Nat.eqb j i then a' else if Nat.eqb j (S i) then b' else nth j v 0) (seq 0 (length v))).
proof: Proof. move=> /step_intro H. elim: i v. { move=> [|? [|? v]] /=; [done|done|]. move=> [->] [->]. have := H [] v. by rewrite -!seq_shift !map_map /= map_nth_seq. } move=> i IH [|? v] /=; first done. move=> /IH /[apply]. rewrite -!seq_shift !map_map /=. move: (map _ _) => ? [] > /step_intro H'. by apply: (H' (_ :: _) _). Qed.
imports: Undecidability.IntersectionTypes.CD Undecidability.IntersectionTypes.Util.CD_facts Undecidability.StringRewriting.SSTS Undecidability.LambdaCalculus.Util.term_facts Relations List PeanoNat Lia ssreflect ssrfun