reconsider t = root-tree [x,s] as Term of S,X by MSATERM:4;
the_sort_of t = s by MSATERM:14;
then t is Element of the Sorts of (FreeMSA X) . s by MSAFREE3:7;
hence root-tree [x,s] is Element of the Sorts of (Free (S,X)) . s by MSAFREE3:31; :: thesis: verum