+ Definition letrec_helper Γ Δ l (varstypes:Tree ??(VV * HaskType Γ ★)) ξ' :
+ ITree (LeveledHaskType Γ ★)
+ (fun t : LeveledHaskType Γ ★ => Expr Γ Δ ξ' t)
+ (mapOptionTree (ξ' ○ (@fst _ _)) varstypes)
+ -> ELetRecBindings Γ Δ ξ' l varstypes.
+ intros.
+ induction varstypes.
+ destruct a; simpl in *.
+ destruct p.
+ simpl.
+ apply ileaf in X. simpl in X.
+ apply ELR_leaf.
+ rename h into τ.
+ destruct (eqd_dec (unlev (ξ' v)) τ).
+ rewrite <- e.
+ destruct (ξ' v).
+ simpl.
+ destruct (eqd_dec h0 l).
+ rewrite <- e0.
+ apply X.
+ apply (Prelude_error "level mismatch; should never happen").
+ apply (Prelude_error "letrec type mismatch; should never happen").
+
+ apply ELR_nil.
+ apply ELR_branch.
+ apply IHvarstypes1; inversion X; auto.
+ apply IHvarstypes2; inversion X; auto.
+ Defined.
+
+ Definition unindex_tree {V}{F} : forall {t:Tree ??V}, ITree V F t -> Tree ??{ v:V & F v }.
+ refine (fix rec t it := match it as IT return Tree ??{ v:V & F v } with
+ | INone => T_Leaf None
+ | ILeaf x y => T_Leaf (Some _)
+ | IBranch _ _ b1 b2 => (rec _ b1),,(rec _ b2)
+ end).
+ exists x; auto.
+ Defined.
+
+ Definition fix_indexing X (F:X->Type)(J:X->Type)(t:Tree ??{ x:X & F x })
+ : ITree { x:X & F x } (fun x => J (projT1 x)) t
+ -> ITree X (fun x:X => J x) (mapOptionTree (@projT1 _ _) t).
+ intro it.
+ induction it; simpl in *.
+ apply INone.
+ apply ILeaf.
+ apply f.
+ simpl; apply IBranch; auto.
+ Defined.
+
+ Definition fix2 {X}{F} : Tree ??{ x:X & FreshM (F x) } -> Tree ??(FreshM { x:X & F x }).
+ refine (fix rec t := match t with
+ | T_Leaf None => T_Leaf None
+ | T_Leaf (Some x) => T_Leaf (Some _)
+ | T_Branch b1 b2 => T_Branch (rec b1) (rec b2)
+ end).
+ destruct x as [x fx].
+ refine (bind fx' = fx ; return _).
+ apply FreshMon.
+ exists x.
+ apply fx'.
+ Defined.
+
+ Definition case_helper tc Γ Δ lev tbranches avars ξ :
+ forall pcb:{sac : StrongAltCon & ProofCaseBranch tc Γ Δ lev tbranches avars sac},
+ prod (judg2exprType (pcb_judg (projT2 pcb))) {vars' : Tree ??VV & pcb_freevars (projT2 pcb) = mapOptionTree ξ vars'} ->
+ ((fun sac => FreshM
+ { scb : StrongCaseBranchWithVVs VV eqdec_vv tc avars sac
+ & Expr (sac_Γ sac Γ) (sac_Δ sac Γ avars (weakCK'' Δ)) (scbwv_ξ scb ξ lev) (weakLT' (tbranches @@ lev)) }) (projT1 pcb)).
+ intro pcb.
+ intro X.
+ simpl in X.
+ simpl.
+ destruct pcb as [sac pcb].
+ simpl in *.
+
+ 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.
+ simpl.
+ unfold scbwv_ξ.
+ rewrite vars_pf.
+ rewrite <- mapOptionTree_compose.
+ clear localvars_pf1.
+ simpl.
+ rewrite mapleaves'.
+
+ admit.
+
+ exists scb.
+ apply ileaf in q.
+ apply q.
+
+ admit.
+ admit.
+ Defined.
+
+ Definition gather_branch_variables
+ Γ Δ (ξ:VV -> LeveledHaskType Γ ★) tc avars tbranches lev (alts:Tree ?? {sac : StrongAltCon &
+ ProofCaseBranch tc Γ Δ lev tbranches avars sac})
+ :
+ forall vars,
+ mapOptionTreeAndFlatten (fun x => pcb_freevars(Γ:=Γ) (projT2 x)) alts = mapOptionTree ξ vars
+ -> ITree Judg judg2exprType (mapOptionTree (fun x => pcb_judg (projT2 x)) alts)
+ -> ITree _ (fun q => prod (judg2exprType (pcb_judg (projT2 q)))
+ { vars' : _ & pcb_freevars (projT2 q) = mapOptionTree ξ vars' })
+ alts.
+ induction alts;
+ intro vars;
+ intro pf;
+ intro source.
+ destruct a; [ idtac | apply INone ].
+ simpl in *.
+ apply ileaf in source.
+ apply ILeaf.
+ destruct s as [sac pcb].
+ simpl in *.
+ split.
+ intros.
+ eapply source.
+ apply H.
+ clear source.
+
+ exists vars.
+ auto.
+
+ simpl in pf.
+ destruct vars; try destruct o; simpl in pf; inversion pf.
+ simpl in source.
+ inversion source.
+ subst.
+ apply IBranch.
+ apply (IHalts1 vars1 H0 X); auto.
+ apply (IHalts2 vars2 H1 X0); auto.
+
+ Defined.
+
+
+ Definition rule2expr : forall h j (r:Rule h j), ITree _ judg2exprType h -> ITree _ judg2exprType j.