Make focus commands work on CoreTC
Allow Transform CoreExprEquality String in proof shell
Allow lemmas to be instantiated to create new lemmas