Bring back wp_bindi

I know we don't use it.  Stating theorems also serves to document things, and IMHO this one is informative.  It also costs us nothing.
1 job for master
Status Job ID Name Coverage
  Test
passed #494
coq
buildjob

00:03:51