Define the relation as
[concrete: C].[P] =>> [concrete: C].[concrete: C : P]
instead of
[concrete: C].[P] =>> [concrete: C : P]
This changes the rewrite loop recorded for a rule T.[concrete: C : P]
to have (T.[concrete: C] => T) appearing twice in context instead of
just once.
We don't ever want a concrete conformance rule to be able to imply a
concrete type rule. This became possible with loop normalization
because the single occurrence of (T.[concrete: C] => T).[P] could
cancel with a subsequent step (T => T.[concrete: C]).[P] in another
rewrite loop after substitution.