+
+Lemma vec2list_injective : forall T n (v1 v2:vec T n), vec2list v1 = vec2list v2 -> v1 = v2.
+ admit.
+ Defined.
+
+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).
+ intros.
+ unfold scbwv_ξ.
+ unfold scbwv_varstypes.
+ set (@update_ξ_lemma _ _ (weakLT' ○ ξ) (weakL' l)
+ (vec2list (vec_zip (scbwv_exprvars scb) (sac_types (scbwv_sac scb) Γ atypes)))) as q.
+ rewrite vec2list_map_list2vec in q.
+ rewrite fst_zip in q.
+ rewrite vec2list_map_list2vec in q.
+ rewrite vec2list_map_list2vec in q.
+ rewrite snd_zip in q.
+ rewrite vec2list_map_list2vec in q.
+ apply vec2list_injective.
+ apply q.
+ apply scbwv_exprvars_distinct.
+ Qed.
+
+Lemma case_lemma : forall Γ Δ ξ l tc tbranches atypes e alts',
+ mapOptionTree ξ (expr2antecedent (ECase Γ Δ ξ l tc tbranches atypes e alts'))
+ = ((mapOptionTreeAndFlatten pcb_freevars (mapOptionTree mkProofCaseBranch alts')),,mapOptionTree ξ (expr2antecedent e)).
+ intros.
+ simpl.
+ Ltac hack := match goal with [ |- ?A,,?B = ?C,,?D ] => assert (A=C) end.
+ hack.
+ induction alts'.
+ simpl.
+ destruct a.
+ unfold mkProofCaseBranch.
+ simpl.
+ reflexivity.
+ reflexivity.
+ simpl.
+ rewrite IHalts'1.
+ rewrite IHalts'2.
+ reflexivity.
+ rewrite H.
+ reflexivity.
+ Qed.
+