+ set (sac_types pcb_scb _ avars) as boundvars.
+ refine (fresh_lemma' _ (unleaves (map (fun x => x@@(weakL' lev)) (vec2list boundvars))) Σ
+ (mapOptionTree weakLT' pcb_freevars)
+ (weakLT' ○ ξ) _
+ >>>= fun ξvars => _). apply FreshMon.
+ rewrite H.
+ rewrite <- mapOptionTree_compose.
+ reflexivity.
+ destruct ξvars as [ exprvars [pf1 pf2 ]].
+ set (list2vec (leaves (mapOptionTree (@fst _ _) exprvars))) as exprvars'.
+ assert (sac_numExprVars pcb_scb = Datatypes.length (leaves (mapOptionTree (@fst _ _) exprvars))) as H'.
+ rewrite <- mapOptionTree_compose in pf2.
+ simpl in pf2.
+ rewrite mapleaves.
+ rewrite <- map_preserves_length.
+ rewrite map_preserves_length with (f:=update_ξ (weakLT' ○ ξ) (leaves exprvars) ○ (@fst _ _)).
+ rewrite <- mapleaves.
+ rewrite pf2.
+ rewrite leaves_unleaves.
+ rewrite vec2list_map_list2vec.
+ rewrite vec2list_len.
+ reflexivity.
+ rewrite <- H' in exprvars'.
+ clear H'.
+
+ set (@Build_StrongCaseBranchWithVVs VV _ tc _ avars pcb_scb exprvars') as scb.
+ set (scbwv_ξ scb ξ lev) as ξ'.
+ refine (X ξ' (Σ,,(unleaves (vec2list exprvars'))) _ >>>= fun X' => return _). apply FreshMon.
+ simpl.
+ unfold ξ'.
+ unfold scbwv_ξ.
+ simpl.
+ rewrite <- vec2list_map_list2vec.
+ rewrite <- pf1.
+ admit.
+
+ apply ileaf in X'.
+ simpl in X'.
+ exists scb.
+ unfold weakCK''.
+ unfold ξ' in X'.
+ apply X'.
+ Defined.
+
+ Fixpoint treeM {T}(t:Tree ??(FreshM T)) : FreshM (Tree ??T) :=
+ match t with
+ | T_Leaf None => return []
+ | T_Leaf (Some x) => bind x' = x ; return [x']
+ | T_Branch b1 b2 => bind b1' = treeM b1 ; bind b2' = treeM b2 ; return (b1',,b2')
+ end.