Sealed: mark seal/unseal as coercions

[mtzguido]

Draft, should test across projects.

[TWal]

I didn't know [@@coercion]! What is it doing?

[mtzguido]

Hi Théophile, sorry, I now realize we didn't have any documentation on them. I started a doc/ref directory where I will place notes about this kind of features (which may not be polished enough for the book). Adding them here https://github.com/FStarLang/FStar/pull/3484, including a note about coercions.

This made me realize these coercions will probably not work so well either, since they are usually not between named types.

[TWal]

Ah excellent, thank you!