len {} = 0 ;
then len (Rev {}) = 0 by Def3;
hence Rev f is empty ; :: thesis: verum