A1: e = (e . {}) -tree (args e) by ARGS;
args e is FinSequence of (Free (S,X)) by A1, Th32;
hence args e is FinSequence of (Free (S,X)) ; :: thesis: verum