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