A proof in Idris that `reverse . reverse = id`

SampleTheorems.idr

module SampleTheorems

%default total

reverse' : List a -> List a
reverse' [] = []
reverse' (x :: xs) = reverse' xs ++ [x]

append_nil : xs ++ [] = xs
append_nil {xs = []} = Refl
append_nil {xs = (y :: ys)} = rewrite append_nil {xs=ys} in Refl

rev_distrib : (xs, ys : List a) -> reverse' (xs ++ ys) = reverse' ys ++ reverse' xs
rev_distrib [] ys = rewrite append_nil {xs=(reverse' ys)} in Refl
rev_distrib (z :: zs) ys = rewrite rev_distrib zs ys in
                           rewrite appendAssociative (reverse' ys) (reverse' zs) [z] in Refl

rev_rev_id : (lst : List a) -> reverse' (reverse' lst) = lst
rev_rev_id [] = Refl
rev_rev_id (x :: xs) = rewrite rev_distrib (reverse' xs) [x] in 
                       rewrite rev_rev_id xs in Refl

Revision 3 is working with Idris 0.11 (current master at least).

Works with 1.0 too