+ apply X0.
+
+ simpl in X0.
+ apply rdrop'' in X0.
+ apply rdrop'''.
+ apply X0.
+
+ intros.
+ simpl in X0.
+ apply rassoc in X0.
+ set (IHΣ₁₂1 _ _ (rdrop _ _ _ _ _ _ X) X0) as q.
+ set (IHΣ₁₂2 _ (Σ₁,,Σ₂) (rdrop' _ _ _ _ _ _ X)) as q'.
+ apply rassoc' in q.
+ apply swapr in q.
+ apply rassoc in q.
+ set (q' q) as q''.
+ apply rassoc' in q''.
+ apply rdup in q''.
+ apply q''.
+ Defined.
+
+ Definition rule2expr : forall h j (r:Rule h j), ITree _ judg2exprType h -> ITree _ judg2exprType j.
+
+ intros h j r.
+
+ refine (match r as R in Rule H C return ITree _ judg2exprType H -> ITree _ judg2exprType C with
+ | RArrange a b c d e l r => let case_RURule := tt in _
+ | RNote Γ Δ Σ τ l n => let case_RNote := tt in _
+ | RLit Γ Δ l _ => let case_RLit := tt in _
+ | RVar Γ Δ σ p => let case_RVar := tt in _
+ | RGlobal Γ Δ σ l wev => let case_RGlobal := tt in _
+ | RLam Γ Δ Σ tx te x => let case_RLam := tt in _
+ | RCast Γ Δ Σ σ τ γ x => let case_RCast := tt in _
+ | RAbsT Γ Δ Σ κ σ a n => let case_RAbsT := tt in _
+ | RAppT Γ Δ Σ κ σ τ y => let case_RAppT := tt in _
+ | RAppCo Γ Δ Σ κ σ₁ σ₂ γ σ l => let case_RAppCo := tt in _
+ | RAbsCo Γ Δ Σ κ σ σ₁ σ₂ y => let case_RAbsCo := tt in _
+ | RApp Γ Δ Σ₁ Σ₂ tx te p => let case_RApp := tt in _
+ | RCut Γ Δ Σ Σ₁ Σ₁₂ Σ₂ Σ₃ l => let case_RCut := tt in _
+ | RLeft Γ Δ Σ₁ Σ₂ Σ l => let case_RLeft := tt in _
+ | RRight Γ Δ Σ₁ Σ₂ Σ l => let case_RRight := tt in _
+ | RVoid _ _ l => let case_RVoid := tt in _
+ | RBrak Σ a b c n m => let case_RBrak := tt in _
+ | REsc Σ a b c n m => let case_REsc := tt in _
+ | RCase Γ Δ lev tc Σ avars tbranches alts => let case_RCase := tt in _
+ | RLetRec Γ Δ lri x y t => let case_RLetRec := tt in _
+ end); intro X_; try apply ileaf in X_; simpl in X_.
+
+ destruct case_RURule.
+ apply ILeaf. simpl. intros.
+ set (@urule2expr a b _ _ e l r0 ξ) as q.
+ unfold ujudg2exprType.
+ unfold ujudg2exprType in q.
+ apply q with (vars:=vars).
+ intros.
+ apply X_ with (vars:=vars0).
+ auto.
+ auto.
+
+ destruct case_RBrak.
+ apply ILeaf; simpl; intros; refine (X_ ξ vars H >>>= fun X => return ILeaf _ _). apply FreshMon.
+ apply EBrak.
+ apply (ileaf X).
+
+ destruct case_REsc.
+ apply ILeaf; simpl; intros; refine (X_ ξ vars H >>>= fun X => return ILeaf _ _). apply FreshMon.
+ apply EEsc.
+ apply (ileaf X).
+
+ destruct case_RNote.
+ apply ILeaf; simpl; intros; refine (X_ ξ vars H >>>= fun X => return ILeaf _ _). apply FreshMon.
+ apply ENote; auto.
+ apply (ileaf X).
+
+ destruct case_RLit.
+ apply ILeaf; simpl; intros; refine (return ILeaf _ _).
+ apply ELit.
+
+ destruct case_RVar.
+ apply ILeaf; simpl; intros; refine (return ILeaf _ _).
+ destruct vars; simpl in H; inversion H; destruct o. inversion H1.
+ set (@EVar _ _ _ Δ ξ v) as q.
+ rewrite <- H2 in q.
+ simpl in q.
+ apply q.
+ inversion H.
+
+ destruct case_RGlobal.
+ apply ILeaf; simpl; intros; refine (return ILeaf _ _).
+ apply EGlobal.
+
+ destruct case_RLam.
+ apply ILeaf.
+ simpl in *; intros.
+ refine (fresh_lemma _ ξ vars _ tx x H >>>= (fun pf => _)).
+ apply FreshMon.
+ destruct pf as [ vnew [ pf1 pf2 ]].
+ set (update_xi ξ x (((vnew, tx )) :: nil)) as ξ' in *.
+ refine (X_ ξ' (vars,,[vnew]) _ >>>= _).
+ apply FreshMon.
+ simpl.
+ rewrite pf1.
+ rewrite <- pf2.
+ simpl.
+ reflexivity.
+ intro hyp.
+ refine (return _).
+ apply ILeaf.
+ apply ELam with (ev:=vnew).
+ apply ileaf in hyp.
+ simpl in hyp.
+ unfold ξ' in hyp.
+ apply hyp.
+
+ destruct case_RCast.
+ apply ILeaf; simpl; intros; refine (X_ ξ vars H >>>= fun X => return ILeaf _ _). apply FreshMon.
+ eapply ECast.
+ apply x.
+ apply ileaf in X. simpl in X.
+ apply X.
+
+ 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_RCut.
+ apply rassoc.
+ apply swapr.
+ apply rassoc'.
+
+ inversion X_.
+ subst.
+ clear X_.
+
+ apply rassoc' in X0.
+ apply swapr in X0.
+ apply rassoc in X0.
+
+ induction Σ₃.
+ destruct a.
+ subst.
+ eapply rcut.
+ apply X.
+ apply X0.
+
+ apply ILeaf.
+ simpl.
+ intros.
+ refine (return _).
+ apply INone.
+ set (IHΣ₃1 (rdrop _ _ _ _ _ _ X0)) as q1.
+ set (IHΣ₃2 (rdrop' _ _ _ _ _ _ X0)) as q2.
+ apply ileaf in q1.
+ apply ileaf in q2.
+ simpl in *.
+ apply ILeaf.
+ simpl.
+ intros.
+ refine (q1 _ _ H >>>= fun q1' => q2 _ _ H >>>= fun q2' => return _).
+ apply FreshMon.
+ apply FreshMon.
+ apply IBranch; auto.
+
+ destruct case_RLeft.
+ apply ILeaf.
+ simpl; intros.
+ destruct vars; try destruct o; inversion H.
+ refine (X_ _ _ H2 >>>= fun X' => return _).
+ apply FreshMon.
+ apply IBranch.
+ eapply vartree.
+ apply H1.
+ apply X'.
+
+ destruct case_RRight.
+ apply ILeaf.
+ simpl; intros.
+ destruct vars; try destruct o; inversion H.
+ refine (X_ _ _ H1 >>>= fun X' => return _).
+ apply FreshMon.
+ apply IBranch.
+ apply X'.
+ eapply vartree.
+ apply H2.
+
+ 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 _ _ _ _ _ _ n).
+ 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_xi ξ t (leaves varstypes)))
+ ((mapOptionTree (@fst _ _) varstypes),,vars) _ >>>= 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 mapOptionTree_compose.
+ rewrite mapOptionTree_compose.
+ rewrite pf2.
+ replace ((mapOptionTree unlev (y @@@ t))) with y.
+ apply X0.
+ clear pf1 X0 X1 pfdist pf2 vars varstypes.
+ induction y; try destruct a; auto.
+ rewrite IHy1 at 1.
+ rewrite IHy2 at 1.
+ reflexivity.
+ apply ileaf in X1.
+ simpl 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.
+
+ Definition proof2expr Γ Δ τ l Σ (ξ0: VV -> LeveledHaskType Γ ★)
+ {zz:ToString VV} : ND Rule [] [Γ > Δ > Σ |- [τ] @ l] ->
+ FreshM (???{ ξ : _ & Expr Γ Δ ξ τ l}).
+ 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 in it.
+ simpl in it.
+ apply it.
+ apply INone.