+ 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
+ | RURule a b c d e => 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 => 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 _
+ | RLet Γ Δ Σ₁ Σ₂ σ₁ σ₂ p => let case_RLet := tt in _
+ | RBindingGroup Γ p lri m x q => let case_RBindingGroup := tt in _
+ | REmptyGroup _ _ => let case_REmptyGroup := 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 => let case_RLetRec := tt in _
+ end); intro X_; try apply ileaf in X_; simpl in X_.
+
+ destruct case_RURule.
+ destruct d; try destruct o.
+ apply ILeaf; destruct u; simpl; intros.
+ set (@urule2expr a b _ _ e ξ) as q.
+ set (fun z => ileaf (q z)) as q'.
+ simpl in q'.
+ apply q' with (vars:=vars).
+ clear q' q.
+ apply bridge.
+ apply X_.
+ auto.
+ apply no_urules_with_empty_conclusion in e; inversion e; auto.
+ apply no_urules_with_multiple_conclusions in e; inversion e; auto; exists d1; exists d2; 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. rewrite H2.
+ apply EVar.
+ inversion H.
+
+ destruct case_RGlobal.
+ apply ILeaf; simpl; intros; refine (return ILeaf _ _).
+ apply EGlobal.
+ apply wev.
+
+ 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_ξ ξ ((⟨vnew, tx @@ x ⟩) :: 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_RBindingGroup.
+ 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 _ ξ vars1 _ (σ₂@@p) H1 >>>= (fun pf => _)).
+ apply FreshMon.
+ destruct pf as [ vnew [ pf1 pf2 ]].
+ set (update_ξ ξ ((⟨vnew, σ₂ @@ p ⟩) :: nil)) as ξ' in *.
+ inversion X_.
+ apply ileaf in X.
+ apply ileaf in X0.
+ simpl in *.
+ refine (X0 ξ vars2 _ >>>= fun X0' => _).
+ apply FreshMon.
+ auto.
+ refine (X ξ' (vars1,,[vnew]) _ >>>= fun X1' => _).
+ apply FreshMon.
+ rewrite H1.
+ simpl.
+ rewrite pf2.
+ rewrite pf1.
+ rewrite H1.
+ reflexivity.
+ refine (return _).
+ apply ILeaf.
+ apply ileaf in X0'.
+ apply ileaf in X1'.
+ simpl in *.
+ apply ELet with (ev:=vnew)(tv:=σ₂).
+ apply X0'.
+ apply X1'.
+
+ destruct case_REmptyGroup.
+ 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 _ _ _ H; _). apply FreshMon.
+ destruct ξvars as [ varstypes [ pf1 pf2 ]].
+ refine (X_ ((update_ξ ξ (leaves varstypes)))
+ (vars,,(mapOptionTree (@fst _ _) varstypes)) _ >>>= fun X => return _); clear X_. apply FreshMon.
+ simpl.
+ rewrite pf2.
+ rewrite pf1.
+ auto.
+ apply ILeaf.
+ destruct x as [τ l].
+ inversion X; subst; clear X.
+
+ (* getting rid of this will require strengthening RLetRec *)
+ assert ((mapOptionTree (fun x : VV * LeveledHaskType Γ ★ => ⟨fst x, unlev (snd x) @@ l ⟩) varstypes) = varstypes) as HHH.
+ admit.
+
+ apply (@ELetRec _ _ _ _ _ _ _ (mapOptionTree (fun x => ((fst x),unlev (snd x))) varstypes));
+ rewrite mapleaves; rewrite <- map_compose; simpl;
+ [ idtac
+ | rewrite <- mapleaves; rewrite HHH; apply (ileaf X0) ].
+
+ clear X0.
+ rewrite <- mapOptionTree_compose in X1.
+ set (fun x : VV * LeveledHaskType Γ ★ => ⟨fst x, unlev (snd x) @@ l ⟩) as ξ' in *.
+ rewrite <- mapleaves.
+ rewrite HHH.
+
+ apply (letrec_helper _ _ _ _ _ X1).
+
+ destruct case_RCase.
+ apply ILeaf; simpl; intros.
+ inversion X_.
+ clear X_.
+ subst.
+ apply ileaf in X0.
+ simpl in X0.
+ set (mapOptionTreeAndFlatten pcb_freevars alts) as Σalts in *.
+ refine (bind ξvars = fresh_lemma' _ (Σalts,,Σ) _ _ _ H ; _).
+ apply FreshMon.
+ destruct vars; try destruct o; inversion H; clear H.
+ rename vars1 into varsalts.
+ rename vars2 into varsΣ.
+
+
+ refine ( _ >>>= fun Y => X0 ξ varsΣ _ >>>= fun X => return ILeaf _ (@ECase _ _ _ _ _ _ _ _ _ (ileaf X) Y)); auto.
+ apply FreshMon.
+ destruct ξvars as [varstypes [pf1 pf2]].
+
+ apply treeM.
+ apply itree_mapOptionTree in X.
+ refine (itree_to_tree (itmap _ X)).
+ intros.
+ eapply case_helper.
+ apply X1.
+ instantiate (1:=varsΣ).
+ rewrite <- H2.
+ admit.
+ apply FreshMon.
+ Defined.
+
+ Definition closed2expr : forall c (pn:@ClosedND _ Rule c), ITree _ judg2exprType c.
+ refine ((
+ fix closed2expr' j (pn:@ClosedND _ Rule j) {struct pn} : ITree _ judg2exprType j :=
+ match pn in @ClosedND _ _ J return ITree _ judg2exprType J with
+ | cnd_weak => let case_nil := tt in INone _ _
+ | cnd_rule h c cnd' r => let case_rule := tt in rule2expr _ _ r (closed2expr' _ cnd')
+ | cnd_branch _ _ c1 c2 => let case_branch := tt in IBranch _ _ (closed2expr' _ c1) (closed2expr' _ c2)
+ end)); clear closed2expr'; intros; subst.
+ Defined.
+
+ Definition proof2expr Γ Δ τ Σ (ξ0: VV -> LeveledHaskType Γ ★)
+ {zz:ToString VV} : ND Rule [] [Γ > Δ > Σ |- [τ]] ->
+ FreshM (???{ ξ : _ & Expr Γ Δ ξ τ}).