proposition: Lemma subst_subst_many_single s n t : subst s n t = subst_many s n [t].
proof: Proof. elim: s n. - move=> x n /=. have [?|[->|Hxn]] : x < n \/ x = n \/ (x - n = S (x - n - 1)) by lia. + rewrite app_nth1. { by rewrite map_length seq_length. } rewrite map_nth seq_nth. { done. } case E: (Nat.eqb _ _); move=> /Nat.eqb_spec in E; [lia|done]. + rewrite Nat.eqb_refl. by rewrite app_nth2 map_length seq_length ?Nat.sub_diag. + case E: (Nat.eqb _ _); move=> /Nat.eqb_spec in E; [lia|]. rewrite app_nth2 map_length seq_length. { lia. } rewrite Hxn /=. by case: (x - n - 1). - by move=> ? + ? + ? /= => -> ->. - by move=> ? + ? /= => ->. Qed.
imports: List Relations Undecidability.L.L Undecidability.L.Util.L_facts ssreflect ssrbool ssrfun