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

assume len f = 0 ; :: thesis: Rev f = f

then f = {} ;

hence Rev f = f ; :: thesis: verum