( n = 0 or n > 0 ) ;
then ( n |-> a is empty or n |-> a is constant ) ;
hence Rev (n |-> a) = n |-> a ; :: thesis: verum