Explicit sharing

[gmalecha]

I'm wondering if it would of interest to provide explicit sharing information in terms. I imagine something like:

tTerm (nm : positive) (t : term) (_ : term)
tRef (nm : positive)

This would act like let-in but would not generate the construct and instead just use the same node.

This would be a way to address https://github.com/coq/coq/issues/11111 but it could also be independently useful.