We will talk about using Lean to provide guarantees about data structures which are useful real world software. In particular, we will look at arrays and vectors. The arrays require a proof obligation for access at a given index. The vectors have their size included in its type. Additionally, we will show how to use…