As already done at most places, only open uPred_scope around definitions. That way there is no need for %C scopes in lemmas anymore.
uPred_scope
%C