Temporary fix for reflection of partial elements.

[marcinjangrzybowski]

Preventing of unfolding definitioons containing face constraints patterns while translating Internal representation to Reflected.

Although this will leak generated definitions, we can still reduce them in macros by applying them to interval ends, assuming we know the type of partial elements (which is the case for tactics where we inspect partial elements as arguments to hcomps). When used in this manner, the names of generated definitions are not leaking outside the macro. I have wrapped this approach into a set of helpers-macros, and from that point, the tactic can be abstracted over that helpers. I tested this in practice with very good results. (link to relevant PR for cubical will follow).

[marcinjangrzybowski]

@plt-amy here is promissed PR to cubical library
agda/cubical#1150

[plt-amy]

Although I'm not happy about leaking some generated extended-lambda names, doing better would require properly integrating the system coverage check with the actual coverage checker, and while that may happen at the upcoming AIM, this is an easy-enough change to revert which prevents the reflection code from spitting nonsense at the user.