Untyped built-in term handling API

[ecranceMERCE]

The term manipulation API functions like fold-map or copy are untyped, i.e., they traverse binders adding untyped bound variables with pi x instead of using @pi-decl .... As discussed, maybe we should propose copy as a typed one by default, and a raw-copy for people wanting to remain at the purely syntactical level without involving the Coq typechecker.