Add a proper dummy constr, instead of using mkProp

[yannl35133]

I was tired of seeing mkProp used transparently as a dummy.
I replaced all uses of it with dummy, then went and checked whether these were dummies or actual uses of Prop.
I am pretty sure for all uses, but this warrants a second opinion.

I'm also not too sure about

rocq/plugins/ssr/ssrfwd.ml

Line 351 in e47214b

let c = EConstr.mkProp in

which, if a dummy, hides it very deep, and

rocq/plugins/ssr/ssrequality.ml

Line 419 in e47214b

let tP = mkLetIn (idA, rdx_ty, tA, mkLetIn (anonR, mkProp, mkType Univ.Universe.type1, tP)) in

which may just need a substitution instead of an apparently useless let-in.

[SkySkimmer]

Isn't that a valid var name? I would be concerned about risk of capture if someone decides to use it in a mknamelambda or some such thing.

[SkySkimmer]

IMO Prop is more likely to be inert than Var

[yannl35133]

I took the names used for debugger printing in CClosure, the name can be changed.
Prop can fly under the radar much longer than Vars; would you rather have a Meta with negative index?

[ppedrot]

FWIW I don't like that change, because the "dumminess" may depend on the context. It's better to keep it local thus.

[yannl35133]

What are the level of dumminess we may want?

• fail on kind that one is probably useless
• fail on reduction
• fail on typing

My issue with the current situation is that Prop fails nowhere.