feat: port modality_embed_mixin and IntoEmbed

[alvinylt]

Description

Addresses #225 in full. Also addresses #219 and #235 in part.

• Modified FromModal so that it is on the same level of generality as the Rocq version. Adjusted the implementation of imodintro to accommodate the generalisation.
• Ported the type class IntoEmbed.
• Ported the two instances of IntoEmbed along with a new instance of FromModal.
• Ported modality_embed and modality_embed_mixin.
• Some relevant tests with imodintro.

Other Changes

Added the missing unpackIprop for Embed so that the iprop(...) wrapper does not get printed in the proof state.

Checklist

• My code follows the mathlib naming and code style conventions
• I have added my name to the authors section of any appropriate files

[MackieLoeffel]

Looks great, thanks!