Turn `mdc_path p ...` predicate into an `p |-> mdc_pathR ...` `Rep`

[pgiarrusso-sl]

Using a Rep notation like mdc_pathR is clearer for readers — both humans and agents.

[pgiarrusso-sl]

cc @gmalecha this came up recently, can we triage it?

[gmalecha]

I see two options:

1. We make a wrapper definition
2. We move Rep into the core definitions.

In the past, I would have advocated for 1 so that we keep Rep outside of the TCB. I am okay if you want to go with 2 though, I think it will require a bit of surgery though.

[pgiarrusso-sl]

Welp, the functors in fmdeps/BRiCk/rocq-skylabs-brick/theories/lang/cpp/logic/pred.v still can't use Rep — but we can add a wrapper in fmdeps/BRiCk/rocq-skylabs-brick/theories/lang/cpp/logic/heap_pred/.