Write a How-to reason about intrinsic syntax using Equations

[thomas-lamiaux]

Write a up to date "How-to reason about intrinsic syntax using Equations" explaining reasoning about intrinsic syntax as usually done in agda, explaining the advantages of Equations and Coq tactic mode.
A good example could be for a (potentially simplified) version of https://dl.acm.org/doi/pdf/10.1145/3158104 that was already ported by Mathieu Sozeau https://github.com/mattam82/Coq-Equations/blob/main/examples/definterp.v

This is a port of the first part of "Intrinsically-Typed Definitional Interpreters for Imperative Languages", Poulsen, Rouvoet, Tolmach, Krebbers and Visser. POPL'18.
It uses well-typed and well-scoped syntax and a monad indexed over an indexed set of stores to define an interpreter for an imperative programming language.
This showcases the use of dependent pattern-matching and pattern-matching lambdas in Equations. We implement a variant where store extension is resolved using type class resolution as well as the dependent-passing style version.