Although I don't plan to bring over new assertions wholesale
into the current qualification branch, it's entirely possible
that various minor changes in main will use the new assertions;
having this basic support in the release branch will simplify that.
(This is why I'm adding the includes as a separate pass from
rewriting the individual assertions)
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.
