<div dir="ltr"><div><div> I hate to advertise for myself twice on the mailing list, but I am currently working on a series of blog posts + videos for Agda beginners, starting with common uses and pitfalls of &quot;with&quot; for functions and proofs. The very next topic I have planned is how to use &quot;inspect&quot;, using as an example the filter function on lists and a proof that all elements of a filtered lists satisfy the predicate used. I plan on doing these tomorrow, and you can find them then from the following links:<br></div><br>Vidya: <a href="https://www.youtube.com/playlist?list=PLWU5W_m7Gj8-CRDXAzQThCf8MSq7wYdff">https://www.youtube.com/playlist?list=PLWU5W_m7Gj8-CRDXAzQThCf8MSq7wYdff</a> (will be titled &quot;with: intro(in)spection&quot;)<br></div>Blag: <a href="http://serendependy.blogspot.com/">http://serendependy.blogspot.com/</a> (same title)<br></div>