[Simplified the correctness proof.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20080514095642] hunk ./ApplicationBased.agda 14
-open SimpleReverse
hunk ./ApplicationBased.agda 125
-  _·_ : forall {a n} -> a ^ n -> Vec a n -> a
-  _·_ {n = zero}  f []       = f
-  _·_ {n = suc n} f (x ∷ xs) = (x <$ n $> f) · xs
-
hunk ./ApplicationBased.agda 126
-  app m f xs          with splitAt m xs
-  app m f .(ys ++ zs) | ys ++' zs = (f · ys) ∷ zs
-
-  app-lemma : forall {a} m {n} x f (s : Vec a (m + n)) ->
-              app m (x <$ m $> f) s ≡ app (suc m) f (x ∷ s)
-  app-lemma m x f s           with splitAt m s
-  app-lemma m x f .(xs ++ ys) | xs ++' ys = ≡-refl
+  app zero    f xs       = f ∷ xs
+  app (suc m) f (x ∷ xs) = app m (x <$ m $> f) xs
hunk ./ApplicationBased.agda 155
-                                  ≡⟨ ≡-cong (exec cs) (app-lemma n x f s) ⟩
+                                  ≡⟨ ≡-refl ⟩