Resolve "Add `Eq` and definitional Proof-Irrelevance"

Closes #57 (closed) Closes #63 (closed)

This MR implements an intensional equality à la MLTT, as well as proof-irrelevance for terms living in Prop, The aim is to extend this definition at a later date by transforming this equality into an observational equality à la CCobs (https://hal.archives-ouvertes.fr/hal-03857705v1). The observational equality can be added as a "drop-in" replacement, as in:

-Eq and Refl will still be axiomatised

-Eq_rec will be encodable through the new cast and transport constructors.