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