proposition: Lemma map_seq_snoc start xs x : map_seq start (xs ++ [x]) =@{M A} <[start+length xs:=x]> (map_seq start xs).
proof: Proof. rewrite map_seq_app, map_seq_singleton. by rewrite insert_union_singleton_r by (by rewrite map_seq_snoc_disjoint). Qed.
imports: Coq(Permutation) stdpp(options)