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.
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.
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.