title:> Doubly Reverse List spec:> /net/beowulf/grad/klin/tmp/list.obj dir:> /net/cs/htdocs/groups/tatami/demos/list/revrev <> ******************************************************** goal:> forall L1:List rev(rev(L1)) = L1 ******************************************************** :> Induction (nil,cons) :> Simplify :> Lemma-Introduction http://www.cs.ucsd.edu/users/klin/tmp/apprev :> Rewriting-Rule :> Simplify <>