+
+ destruct case_RJoin.
+ apply ILeaf; simpl; intros.
+ inversion X_.
+ apply ileaf in X.
+ apply ileaf in X0.
+ simpl in *.
+ destruct vars; inversion H.
+ destruct o; inversion H3.
+ refine (X ξ vars1 H3 >>>= fun X' => X0 ξ vars2 H4 >>>= fun X0' => return _).
+ apply FreshMon.
+ apply FreshMon.
+ apply IBranch; auto.
+
+ destruct case_RApp.
+ apply ILeaf.
+ inversion X_.
+ inversion X.
+ inversion X0.
+ simpl in *.
+ intros.
+ destruct vars. try destruct o; inversion H.
+ simpl in H.
+ inversion H.
+ set (X1 ξ vars1 H5) as q1.
+ set (X2 ξ vars2 H6) as q2.
+ refine (q1 >>>= fun q1' => q2 >>>= fun q2' => return _).
+ apply FreshMon.
+ apply FreshMon.
+ apply ILeaf.
+ apply ileaf in q1'.
+ apply ileaf in q2'.
+ simpl in *.
+ apply (EApp _ _ _ _ _ _ q1' q2').
+
+ destruct case_RLet.
+ apply ILeaf.
+ simpl in *; intros.
+ destruct vars; try destruct o; inversion H.
+
+ refine (fresh_lemma _ ξ _ _ σ₁ p H2 >>>= (fun pf => _)).
+ apply FreshMon.
+
+ destruct pf as [ vnew [ pf1 pf2 ]].
+ set (update_ξ ξ p (((vnew, σ₁ )) :: nil)) as ξ' in *.
+ inversion X_.
+ apply ileaf in X.
+ apply ileaf in X0.
+ simpl in *.
+
+ refine (X ξ vars1 _ >>>= fun X0' => _).
+ apply FreshMon.
+ simpl.
+ auto.
+
+ refine (X0 ξ' ([vnew],,vars2) _ >>>= fun X1' => _).
+ apply FreshMon.
+ simpl.
+ rewrite pf2.
+ rewrite pf1.
+ reflexivity.
+ apply FreshMon.
+
+ apply ILeaf.
+ apply ileaf in X1'.
+ apply ileaf in X0'.
+ simpl in *.
+ apply ELet with (ev:=vnew)(tv:=σ₁).
+ apply X0'.
+ apply X1'.
+
+ destruct case_RWhere.
+ apply ILeaf.
+ simpl in *; intros.
+ destruct vars; try destruct o; inversion H.
+ destruct vars2; try destruct o; inversion H2.
+ clear H2.
+
+ assert ((Σ₁,,Σ₃) = mapOptionTree ξ (vars1,,vars2_2)) as H13; simpl; subst; auto.
+ refine (fresh_lemma _ ξ _ _ σ₁ p H13 >>>= (fun pf => _)).
+ apply FreshMon.
+
+ destruct pf as [ vnew [ pf1 pf2 ]].
+ set (update_ξ ξ p (((vnew, σ₁ )) :: nil)) as ξ' in *.
+ inversion X_.
+ apply ileaf in X.
+ apply ileaf in X0.
+ simpl in *.
+
+ refine (X ξ' (vars1,,([vnew],,vars2_2)) _ >>>= fun X0' => _).
+ apply FreshMon.
+ simpl.
+ inversion pf1.
+ rewrite H3.
+ rewrite H4.
+ rewrite pf2.
+ reflexivity.
+
+ refine (X0 ξ vars2_1 _ >>>= fun X1' => _).
+ apply FreshMon.
+ reflexivity.
+ apply FreshMon.
+
+ apply ILeaf.
+ apply ileaf in X0'.
+ apply ileaf in X1'.
+ simpl in *.
+ apply ELet with (ev:=vnew)(tv:=σ₁).
+ apply X1'.
+ apply X0'.
+
+ destruct case_RVoid.
+ apply ILeaf; simpl; intros.
+ refine (return _).
+ apply INone.
+
+ destruct case_RAppT.
+ apply ILeaf; simpl; intros; refine (X_ ξ vars H >>>= fun X => return ILeaf _ _). apply FreshMon.
+ apply ETyApp.
+ apply (ileaf X).
+
+ destruct case_RAbsT.
+ apply ILeaf; simpl; intros; refine (X_ (weakLT ○ ξ) vars _ >>>= fun X => return ILeaf _ _). apply FreshMon.
+ rewrite mapOptionTree_compose.
+ rewrite <- H.
+ reflexivity.
+ apply ileaf in X. simpl in *.
+ apply ETyLam.
+ apply X.
+
+ destruct case_RAppCo.
+ apply ILeaf; simpl; intros; refine (X_ ξ vars _ >>>= fun X => return ILeaf _ _). apply FreshMon.
+ auto.
+ eapply ECoApp.
+ apply γ.
+ apply (ileaf X).
+
+ destruct case_RAbsCo.
+ apply ILeaf; simpl; intros; refine (X_ ξ vars _ >>>= fun X => return ILeaf _ _). apply FreshMon.
+ auto.
+ eapply ECoLam.
+ apply (ileaf X).
+
+ destruct case_RLetRec.
+ apply ILeaf; simpl; intros.
+ refine (bind ξvars = fresh_lemma' _ y _ _ _ t H; _). apply FreshMon.
+ destruct ξvars as [ varstypes [ pf1[ pf2 pfdist]]].
+ refine (X_ ((update_ξ ξ t (leaves varstypes)))
+ (vars,,(mapOptionTree (@fst _ _) varstypes)) _ >>>= fun X => return _); clear X_. apply FreshMon.
+ simpl.
+ rewrite pf2.
+ rewrite pf1.
+ auto.
+ apply ILeaf.
+ inversion X; subst; clear X.
+
+ apply (@ELetRec _ _ _ _ _ _ _ varstypes).
+ auto.
+ apply (@letrec_helper Γ Δ t varstypes).
+ rewrite <- pf2 in X0.
+ rewrite mapOptionTree_compose.
+ apply X0.
+ apply ileaf in X1.
+ apply X1.
+
+ destruct case_RCase.
+ apply ILeaf; simpl; intros.
+ inversion X_.
+ clear X_.
+ subst.
+ apply ileaf in X0.
+ simpl in X0.
+
+ (* body_freevars and alts_freevars are the types of variables in the body and alternatives (respectively) which are free
+ * from the viewpoint just outside the case block -- i.e. not bound by any of the branches *)
+ rename Σ into body_freevars_types.
+ rename vars into all_freevars.
+ rename X0 into body_expr.
+ rename X into alts_exprs.
+
+ destruct all_freevars; try destruct o; inversion H.
+ rename all_freevars2 into body_freevars.
+ rename all_freevars1 into alts_freevars.
+
+ set (gather_branch_variables _ _ _ _ _ _ _ _ _ H1 alts_exprs) as q.
+ set (itmap (fun pcb alt_expr => case_helper tc Γ Δ lev tbranches avars ξ pcb alt_expr) q) as alts_exprs'.
+ apply fix_indexing in alts_exprs'.
+ simpl in alts_exprs'.
+ apply unindex_tree in alts_exprs'.
+ simpl in alts_exprs'.
+ apply fix2 in alts_exprs'.
+ apply treeM in alts_exprs'.
+
+ refine ( alts_exprs' >>>= fun Y =>
+ body_expr ξ _ _
+ >>>= fun X => return ILeaf _ (@ECase _ _ _ _ _ _ _ _ _ (ileaf X) Y)); auto.
+ apply FreshMon.
+ apply FreshMon.
+ apply H2.
+ Defined.
+
+ Fixpoint closed2expr h j (pn:@SIND _ Rule h j) {struct pn} : ITree _ judg2exprType h -> ITree _ judg2exprType j :=
+ match pn in @SIND _ _ H J return ITree _ judg2exprType H -> ITree _ judg2exprType J with
+ | scnd_weak _ => let case_nil := tt in fun _ => INone _ _
+ | scnd_comp x h c cnd' r => let case_rule := tt in fun q => rule2expr _ _ r (closed2expr _ _ cnd' q)
+ | scnd_branch _ _ _ c1 c2 => let case_branch := tt in fun q => IBranch _ _ (closed2expr _ _ c1 q) (closed2expr _ _ c2 q)
+ end.
+
+ Lemma manyFresh : forall Γ Σ (ξ0:VV -> LeveledHaskType Γ ★),
+ FreshM { vars : _ & { ξ : VV -> LeveledHaskType Γ ★ & Σ = mapOptionTree ξ vars } }.
+ intros Γ Σ.
+ induction Σ; intro ξ.
+ destruct a.
+ destruct l as [τ l].
+ set (fresh_lemma' Γ [τ] [] [] ξ l (refl_equal _)) as q.
+ refine (q >>>= fun q' => return _).
+ apply FreshMon.
+ clear q.
+ destruct q' as [varstypes [pf1 [pf2 distpf]]].
+ exists (mapOptionTree (@fst _ _) varstypes).
+ exists (update_ξ ξ l (leaves varstypes)).
+ symmetry; auto.
+ refine (return _).
+ exists [].
+ exists ξ; auto.
+ refine (bind f1 = IHΣ1 ξ ; _).
+ apply FreshMon.
+ destruct f1 as [vars1 [ξ1 pf1]].
+ refine (bind f2 = IHΣ2 ξ1 ; _).
+ apply FreshMon.
+ destruct f2 as [vars2 [ξ2 pf22]].
+ refine (return _).
+ exists (vars1,,vars2).
+ exists ξ2.
+ simpl.
+ rewrite pf22.
+ rewrite pf1.
+ admit.
+ Defined.
+
+ Definition proof2expr Γ Δ τ Σ (ξ0: VV -> LeveledHaskType Γ ★)
+ {zz:ToString VV} : ND Rule [] [Γ > Δ > Σ |- [τ]] ->
+ FreshM (???{ ξ : _ & Expr Γ Δ ξ τ}).
+ intro pf.
+ set (mkSIND systemfc_all_rules_one_conclusion _ _ _ pf (scnd_weak [])) as cnd.
+ apply closed2expr in cnd.
+ apply ileaf in cnd.
+ simpl in *.
+ clear pf.
+ refine (bind ξvars = manyFresh _ Σ ξ0; _).
+ apply FreshMon.
+ destruct ξvars as [vars ξpf].
+ destruct ξpf as [ξ pf].
+ refine (cnd ξ vars _ >>>= fun it => _).
+ apply FreshMon.
+ auto.
+ refine (return OK _).
+ exists ξ.
+ apply (ileaf it).
+ apply INone.