[saw-core-coq] Fix weird universe constraints generated in SAWCorePreludeExtra

[m-yac]

For some reason, a call to f_equal in the proof of unfold_fold_IRT was generating the constraint prod.u0 < eq.u0, which was causing problems when interacting with returnM_injective in CompMExtra, which generates the constraints:

eq.u0 = Coq.Relations.Relation_Definitions.1 <= prod.u0

Perhaps a better long-term solution is to figure out why returnM_injective generates these constraints and potentially modify it (I suspect it has to do with the use of ~=, which is an operator we need to revisit anyway due to its overlap with the notation for JMEq), but an easy short-term fix is just to modify the proof of unfold_fold_IRT to not use f_equal.

[robdockins]

Looks good to me.

I took the liberty of adding a file that just imports everything else so we can more easily notice in the future if a similar universe problem arises.

[m-yac]

Looks great, thanks Rob!