Allows to replay Coq proofs correctly
There is still a problem with goal names containing spaces such as
those generated by VC generator

move old fnT+fnF versions of t_map, t_fold, etc. to a submodule

Rename as little as possible and keep the API.
Make all the necessary checks in Term and Decl.
Remove the duplicate code in Term but keep it elsewhere.
We will factorize the code as we go, without rush.

I love static typing!

My birthday gift for François.