let f be FinSequence; :: thesis: ( len f = 0 implies Rev f = f )
assume len f = 0 ; :: thesis: Rev f = f
then f = {} ;
hence Rev f = f ; :: thesis: verum