X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FGeneral.v;h=25856d12ca0fc44fea4683093dfd46ba2114acaf;hp=6cb18becc1f882df7b938e6e015c6a2ee2083e79;hb=f60f9ed58ad2ea12fd293dfbcc015c3ffb827a20;hpb=8cb97991a95d5761a28ca94767b8fe637d1411d9

diff --git a/src/General.v b/src/General.v
index 6cb18be..25856d1 100644
--- a/src/General.v
+++ b/src/General.v
@@ -906,14 +906,9 @@ Lemma unleaves_injective : forall T (t1 t2:list T), unleaves t1 = unleaves t2 ->
   reflexivity.
   Qed.
 
-Lemma fst_zip : forall T Q n (v1:vec T n)(v2:vec Q n), vec_map (@fst _ _) (vec_zip v1 v2) = v1.
-  admit.
-  Defined.
-
-Lemma snd_zip : forall T Q n (v1:vec T n)(v2:vec Q n), vec_map (@snd _ _) (vec_zip v1 v2) = v2.
-  admit.
-  Defined.
-
+(* gee I wish I knew how to get Coq to accept these... *)
+Axiom fst_zip : forall T Q n (v1:vec T n)(v2:vec Q n), vec_map (@fst _ _) (vec_zip v1 v2) = v1.
+Axiom snd_zip : forall T Q n (v1:vec T n)(v2:vec Q n), vec_map (@snd _ _) (vec_zip v1 v2) = v2.
 
 Fixpoint mapM {M}{mon:Monad M}{T}(ml:list (M T)) : M (list T) :=
   match ml with