proposition: Lemma step_symbols v w : step rs v w -> (forall i : nat, In (nth i v 0) symbols) -> (forall i : nat, In (nth i w 0) symbols).
proof: Proof. case=> u1 u2 > Hr H i. move: (H i). have [Hi|[->|[->|Hi]]] : i < length u1 \/ i = length u1 \/ i = S (length u1) \/ i >= length u1 + 2 by lia. - by rewrite !(@app_nth1 nat). - move=> _. rewrite (@app_nth2 nat) ?Nat.sub_diag. { done. } apply /in_app_iff. left. apply /in_flat_map. eexists. split; [eassumption|]. move=> /=. tauto. - move=> _. rewrite (@app_nth2 nat). { lia. } have -> : S (length u1) - length u1 = 1 by lia. apply /in_app_iff. left. apply /in_flat_map. eexists. split; [eassumption|]. move=> /=. tauto. - rewrite (@app_nth2 nat). { lia. } rewrite (@app_nth2 nat). { lia. } by have -> : i - length u1 = S (S (i - length u1 - 2)) by lia. Qed.
imports: Undecidability.IntersectionTypes.CD Undecidability.IntersectionTypes.Util.CD_facts Undecidability.StringRewriting.SSTS Undecidability.LambdaCalculus.Util.term_facts Relations List PeanoNat Lia ssreflect ssrfun