Prove map2_append

1 files changed, 7 insertions, 2 deletions

diff --git a/src/Util/CPSUtil.v b/src/Util/CPSUtil.v
index adae0406b..506cda2e7 100644
--- a/src/Util/CPSUtil.v
+++ b/src/Util/CPSUtil.v
@@ -276,11 +276,16 @@ Module Tuple.
     | S n' => fun xs ys T f =>
                 map2_cps g (tl xs) (tl ys) (fun zs => f (append (g (hd xs) (hd ys)) zs))
     end.
-  
+
   Lemma map2_append n A B C f xs ys x y :
     @map2 (S n) A B C f (append x xs) (append y ys)
     = append (f x y) (map2 f xs ys).
-  Admitted.
+  Proof.
+    destruct n; try reflexivity.
+    cbn [append].
+    rewrite map2_S'.
+    reflexivity.
+  Qed.
   Lemma map2_cps_correct {n A B C} g xs ys : forall {T} f,
       @map2_cps n A B C g xs ys T f = f (map2 g xs ys).
   Proof.