#+title: BitEQ
#+author: Yann Herklotz

Reasoning about bit equality for various rewrites.  This is based on [[file:resources/samc.lisp][proofs]] done in ACL2, and uses
the =bbv= library to convert the proofs into Coq.