register and check the type of every builtin

[fblanqui]

• rename "P" into "Prf", "T" into "El", and "and" into "compose" to not clash with the builtin "and" used in why3 tactic
• change types of tactic builtins by using universes to handle \tau and \pi uniformly (add Univ.v lambdapi-stdlib#67)
• builtin.ml: factorize and simplify type checking of builtins, and add type checking of why3 tactic builtins
• rewrite.ml: move builtin type checking to builtin.ml
• enforce the declaration of builtins
• doc on tacticals: update the types of builtins
• tactic.ml: fix handling of "change" in tac_eval
• move the contents of fol.ml into why3_tactic.ml
• update stdlib files in tests/OK

TODO:

• update inverse to get rid of unif_rules
• defines \pi and \tau from \eta ?