X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FGeneral.v;h=2a1a398b5576d40548733415ced4c084ad3d4c6d;hp=055a39a4086c39cf57fe32123559a84fc77f1f68;hb=b3214686b18b2d6f6905394494da8d1c17587bdb;hpb=96ea5272fe6ec62022351f69289eedd330322eb4

diff --git a/src/General.v b/src/General.v
index 055a39a..2a1a398 100644
--- a/src/General.v
+++ b/src/General.v
@@ -876,17 +876,24 @@ Ltac eqd_dec_refl X :=
   destruct (eqd_dec X X) as [eqd_dec1 | eqd_dec2];
     [ clear eqd_dec1 | set (eqd_dec2 (refl_equal _)) as eqd_dec2'; inversion eqd_dec2' ].
 
-Lemma vec2list_injective : forall T n (v1 v2:vec T n), vec2list v1 = vec2list v2 -> v1 = v2.
-  admit.
-  Defined.
-
 Lemma unleaves_injective : forall T (t1 t2:list T), unleaves t1 = unleaves t2 -> t1 = t2.
-  admit.
+  intros T.
+  induction t1; intros.
+  destruct t2.
+  auto.
+  inversion H.
+  destruct t2.
+  inversion H.
+  simpl in H.
+  inversion H.
+  set (IHt1 _ H2) as q.
+  rewrite q.
+  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.
-  Qed.
+  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.