t in the Sorts of (Free (C,(MSVars C))) . (a_Type C) by Def28;
then t at f in the Sorts of (Free (C,(MSVars C))) . (a_Type C) by Th129;
hence t at f is expression of C, a_Type C by Th41; :: thesis: verum