let t1, t2 be FinSequence; :: thesis: ( Rev t1 = Rev t2 implies t1 = t2 )
assume A1: Rev t1 = Rev t2 ; :: thesis: t1 = t2
thus t1 = Rev (Rev t1)
.= t2 by A1 ; :: thesis: verum