%!TEX root = ../Main.tex
\section{Formalization}

Technical notes on the formalization. We make heavy use of the @Forall@ and @Forall2@ types from the Coq base library, along with a large number of reusable impedance matching lemmas that we have proved ourselves. Being functional programmers we try to factor out common recurrences into higher order combinators, rather than repeating patterns of recursion in the language definition and associated proof.

\TODO{Have to deal with indirect mutual recursion, but tradeoff is can use reusable polymorphic relations on lists. Talk about Forall2 lemmas, where they are used, what are some lemmas, why aren't these in the base library. Not easy to discover how to handle this. Not in software foundations. Name other places this isn't in.}

