len (apply (p,t)) = (len p) + 1 by Def19;
hence not apply (p,t) is empty ; :: thesis: verum