remove vec2list_injective

diff --git a/src/General.v b/src/General.v
index 055a39a..4e73755 100644 (file)
--- a/src/General.v
+++ b/src/General.v
@@ -876,12 +876,19 @@ 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.

diff --git a/src/HaskStrongToProof.v b/src/HaskStrongToProof.v
index 0933be2..fa7dcae 100644 (file)
--- a/src/HaskStrongToProof.v
+++ b/src/HaskStrongToProof.v
@@ -695,8 +695,9 @@ Lemma letRecSubproofsToND' Γ Δ ξ lev τ tree  :
 
 Lemma scbwv_coherent {tc}{Γ}{atypes:IList _ (HaskType Γ) _} :
   forall scb:StrongCaseBranchWithVVs _ _ tc atypes,
-    forall l ξ, vec_map (scbwv_ξ scb ξ l) (scbwv_exprvars scb) =
-                                 vec_map (fun t => t @@ weakL' l) (sac_types (scbwv_sac scb) _ atypes).
+    forall l ξ,
+      vec2list (vec_map (scbwv_ξ scb ξ l) (scbwv_exprvars scb)) =
+      vec2list (vec_map (fun t => t @@ weakL' l) (sac_types (scbwv_sac scb) _ atypes)).
   intros.
   unfold scbwv_ξ.
   unfold scbwv_varstypes.
@@ -716,7 +717,6 @@ Lemma scbwv_coherent {tc}{Γ}{atypes:IList _ (HaskType Γ) _} :
   rewrite leaves_unleaves in q'.
   rewrite vec2list_map_list2vec in q'.
   rewrite vec2list_map_list2vec in q'.
-  apply vec2list_injective.
   apply q'.
   rewrite fst_zip.
   apply scbwv_exprvars_distinct.