Add test that the kernel checks relevances in Case binders

[SkySkimmer]

Before 6fae78c (8.17) relevance of Case binders was checked by checking the lambdas produced by expand_case.

Before 0cfe16a (8.18) expand_case would use the relevance from the Case instead of from the inductive data (after it used the relevance from the inductive unsubstituted by the univ instance until 269daf2 (9.0)).

If we had skipped 6fae78c the later patches would have introduced an inconsstency as typechecking would have trusted the Case relevances, but they would be used in conversion.

I think it's worth a test to ensure we don't introduce this possible bug by mistake.

To make testing practical the check is turned into a regular error instead of assert failure.
The test is an output test as otherwise we risk producing some other error if something changes.

[yannl35133]

Can you add the check there as well?

rocq/kernel/environ.ml

Lines 314 to 316 in 5a4f0c2

	Context.
	{ binder_name = nas.(i).binder_name;
	binder_relevance = UVars.subst_instance_relevance u na.binder_relevance }

(maybe the functions can even be merged together)

[SkySkimmer]

Can you add the check there as well?

Is that expected to be called on unchecked data?