proposition: Lemma subst_many_nil s n : subst_many s n [] = s.
proof: Proof. elim: s n. - move=> x n /=. rewrite app_nil_r map_nth. congr var. have [?|?] : x < n \/ n <= x by lia. + by apply seq_nth. + apply nth_overflow. by rewrite seq_length. - by move=> /= ? + ? + ? => -> ->. - by move=> /= ? + ? => ->. Qed.
imports: List Relations Undecidability.L.L Undecidability.L.Util.L_facts ssreflect ssrbool ssrfun