[Agda] Newbie question, book exercise problem.

[Nicolas Pouillard]

Excerpts from Julian Beaumont's message of Mon Nov 30 09:53:44 +0100 2009:
> It's worth pointing out that you can do this fairly simply without
> using EqReasoning. The downside is that the proof is generally less
> readable. Agda will reduce all functions using the definitions as much
> as possible for you. In the inductive case this means the goal is
> simplified to proving x :: tabulate (_!_ xs) == x :: xs. This may be
> proven trivially using cong and a recursive call to lem-tab-!.
> 
> cong : {A B : Set} {x y : A} (f : A -> B) -> x == y -> f x == f y
> cong f refl = refl
> 
> lem-tab-! [] = refl
> lem-tab-! (x :: xs) = cong {! !} {! !} -- you should be able to fill
> in the blanks easily enough.

I've done it myself with cong. However I wanted to make use of the new
'rewrite' feature in the Agda dev version and couldn't make it.
If it is possible I would like to see how...

-- 
Nicolas Pouillard
http://nicolaspouillard.fr