- set (sac_types pcb_scb _ avars) as boundvars.
- refine (fresh_lemma' _ (unleaves (vec2list boundvars)) Σ (mapOptionTree weakLT' pcb_freevars) (weakLT' ○ ξ) (weakL' lev) _
- >>>= fun ξvars => _). apply FreshMon.
- rewrite H.
- rewrite <- mapOptionTree_compose.
- reflexivity.
- destruct ξvars as [ exprvars [pf1 [pf2 pfdistinct]]].
- set (list2vec (leaves (mapOptionTree (@fst _ _) exprvars))) as exprvars'.
-
- assert (distinct (vec2list exprvars')) as pfdistinct'.
- unfold exprvars'.
- rewrite vec2list_list2vec.
- apply pfdistinct.
-
- 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_ξ VV eqdec_vv (@sac_Γ tc pcb_scb Γ)
- (@weakLT' Γ (@vec2list (@sac_numExTyVars tc pcb_scb) Kind (@sac_ekinds tc pcb_scb)) ★ ○ ξ)
- (@weakL' Γ (@vec2list (@sac_numExTyVars tc pcb_scb) Kind (@sac_ekinds tc pcb_scb)) lev)
- (@leaves (VV * HaskType (@sac_Γ tc pcb_scb Γ) ★) exprvars) ○ @fst VV (HaskType (@sac_Γ tc pcb_scb Γ) ★))).
- rewrite <- mapleaves.
- rewrite pf2.
- rewrite <- mapleaves'.
- rewrite leaves_unleaves.
- rewrite vec2list_map_list2vec.
- rewrite vec2list_len.
- reflexivity.
-
- clear pfdistinct'.
- rewrite <- H' in exprvars'.
- clear H'.
- assert (distinct (vec2list exprvars')) as pfdistinct'.
- admit.
-
- set (@Build_StrongCaseBranchWithVVs VV _ tc _ avars pcb_scb exprvars' pfdistinct') 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.