Recommendations in using the API:

The type of terms: constr (see kernel/constr.ml and kernel/term.ml)

- On type constr, the canonical equality on CIC (up to
  alpha-conversion and cast removal) is Constr.equal
- The type constr is abstract, use mkRel, mkSort, etc. to build
  elements in constr; use "kind_of_term" to analyze the head of a
  constr; use destRel, destSort, etc. when the head constructor is
  known