- 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.
+
+ destruct X.
+ destruct s as [vars vars_pf].
+
+ refine (bind localvars = fresh_lemma' _ (unleaves (vec2list (sac_types sac _ avars))) vars
+ (mapOptionTree weakLT' (pcb_freevars pcb)) (weakLT' ○ ξ) (weakL' lev) _ ; _).
+ apply FreshMon.
+ rewrite vars_pf.
+ rewrite <- mapOptionTree_compose.
+ reflexivity.
+ destruct localvars as [localvars [localvars_pf1 [localvars_pf2 localvars_dist ]]].
+ set (mapOptionTree (@fst _ _) localvars) as localvars'.
+
+ set (list2vec (leaves localvars')) as localvars''.
+ cut (length (leaves localvars') = sac_numExprVars sac). intro H''.
+ rewrite H'' in localvars''.
+ cut (distinct (vec2list localvars'')). intro H'''.
+ set (@Build_StrongCaseBranchWithVVs _ _ _ _ avars sac localvars'' H''') as scb.
+
+ refine (bind q = (f (scbwv_ξ scb ξ lev) (vars,,(unleaves (vec2list (scbwv_exprvars scb)))) _) ; return _).
+ apply FreshMon.