new cast: CACHEcast, new tactical: tclCHECKANDCACHE (BUGS)

BUGS:

* the tclABSTRACT before reduct_in_concl exposes to the reduction
  machinery some lets by pulling them in the concl, hence lazy-zeta
  reduces more.

* a proof produced by an STM worker invalidates the signate: leq_env
  used ==

MSG:

The kernel can sign a term that has been typecked
(by the kernel) during proof construction and avoid
type checking it again during Qed.

Example of tclCHECKANDCACHE:
  check_and_cache (vm_cast_no_check (eq_refl w)).
runs the (kernel) vm during proof construction and signs the
resuting term.  At Qed time, if the signature is verified,
the vm is not run again.
This is a relevant optimization for reflexive tactics like ring.