+ 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_xi ξ 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'.
+ Defined.
+
+ Definition vartree Γ Δ Σ lev ξ :
+ forall vars, Σ @@@ lev = mapOptionTree ξ vars ->
+ ITree (HaskType Γ ★) (fun t : HaskType Γ ★ => Expr Γ Δ ξ t lev) Σ.
+ induction Σ; intros.
+ destruct a.
+ intros; simpl in *.
+ apply ILeaf.
+ destruct vars; try destruct o; inversion H.
+ set (EVar Γ Δ ξ v) as q.
+ rewrite <- H1 in q.
+ apply q.
+ intros.
+ apply INone.
+ intros.
+ destruct vars; try destruct o; inversion H.
+ apply IBranch.
+ eapply IHΣ1.
+ apply H1.
+ eapply IHΣ2.
+ apply H2.
+ Defined.
+
+
+ Definition rdrop Γ Δ Σ₁ Σ₁₂ a lev :
+ ITree Judg judg2exprType [Γ > Δ > Σ₁ |- a,,Σ₁₂ @ lev] ->
+ ITree Judg judg2exprType [Γ > Δ > Σ₁ |- a @ lev].
+ intros.
+ apply ileaf in X.
+ apply ILeaf.
+ simpl in *.
+ intros.
+ set (X ξ vars H) as q.
+ simpl in q.
+ refine (q >>>= fun q' => return _).
+ apply FreshMon.
+ inversion q'.
+ apply X0.
+ Defined.
+
+ Definition rdrop' Γ Δ Σ₁ Σ₁₂ a lev :
+ ITree Judg judg2exprType [Γ > Δ > Σ₁ |- Σ₁₂,,a @ lev] ->
+ ITree Judg judg2exprType [Γ > Δ > Σ₁ |- a @ lev].
+ intros.
+ apply ileaf in X.
+ apply ILeaf.
+ simpl in *.
+ intros.
+ set (X ξ vars H) as q.
+ simpl in q.
+ refine (q >>>= fun q' => return _).
+ apply FreshMon.
+ inversion q'.
+ auto.
+ Defined.
+
+ Definition rdrop'' Γ Δ Σ₁ Σ₁₂ lev :
+ ITree Judg judg2exprType [Γ > Δ > [],,Σ₁ |- Σ₁₂ @ lev] ->
+ ITree Judg judg2exprType [Γ > Δ > Σ₁ |- Σ₁₂ @ lev].
+ intros.
+ apply ileaf in X.
+ apply ILeaf.
+ simpl in *; intros.
+ eapply X with (vars:=[],,vars).
+ rewrite H; reflexivity.
+ Defined.
+
+ Definition rdrop''' Γ Δ a Σ₁ Σ₁₂ lev :
+ ITree Judg judg2exprType [Γ > Δ > Σ₁ |- Σ₁₂ @ lev] ->
+ ITree Judg judg2exprType [Γ > Δ > a,,Σ₁ |- Σ₁₂ @ lev].
+ intros.
+ apply ileaf in X.
+ apply ILeaf.
+ simpl in *; intros.
+ destruct vars; try destruct o; inversion H.
+ eapply X with (vars:=vars2).
+ auto.
+ Defined.
+
+ Definition rassoc Γ Δ Σ₁ a b c lev :
+ ITree Judg judg2exprType [Γ > Δ > ((a,,b),,c) |- Σ₁ @ lev] ->
+ ITree Judg judg2exprType [Γ > Δ > (a,,(b,,c)) |- Σ₁ @ lev].
+ intros.
+ apply ileaf in X.
+ apply ILeaf.
+ simpl in *; intros.
+ destruct vars; try destruct o; inversion H.
+ destruct vars2; try destruct o; inversion H2.
+ apply X with (vars:=(vars1,,vars2_1),,vars2_2).
+ subst; reflexivity.
+ Defined.
+
+ Definition rassoc' Γ Δ Σ₁ a b c lev :
+ ITree Judg judg2exprType [Γ > Δ > (a,,(b,,c)) |- Σ₁ @ lev] ->
+ ITree Judg judg2exprType [Γ > Δ > ((a,,b),,c) |- Σ₁ @ lev].
+ intros.
+ apply ileaf in X.
+ apply ILeaf.
+ simpl in *; intros.
+ destruct vars; try destruct o; inversion H.
+ destruct vars1; try destruct o; inversion H1.
+ apply X with (vars:=vars1_1,,(vars1_2,,vars2)).
+ subst; reflexivity.
+ Defined.
+
+ Definition swapr Γ Δ Σ₁ a b c lev :
+ ITree Judg judg2exprType [Γ > Δ > ((a,,b),,c) |- Σ₁ @ lev] ->
+ ITree Judg judg2exprType [Γ > Δ > ((b,,a),,c) |- Σ₁ @ lev].
+ intros.
+ apply ileaf in X.
+ apply ILeaf.
+ simpl in *; intros.
+ destruct vars; try destruct o; inversion H.
+ destruct vars1; try destruct o; inversion H1.
+ apply X with (vars:=(vars1_2,,vars1_1),,vars2).
+ subst; reflexivity.
+ Defined.
+
+ Definition rdup Γ Δ Σ₁ a c lev :
+ ITree Judg judg2exprType [Γ > Δ > ((a,,a),,c) |- Σ₁ @ lev] ->
+ ITree Judg judg2exprType [Γ > Δ > (a,,c) |- Σ₁ @ lev].
+ intros.
+ apply ileaf in X.
+ apply ILeaf.
+ simpl in *; intros.
+ destruct vars; try destruct o; inversion H.
+ apply X with (vars:=(vars1,,vars1),,vars2). (* is this allowed? *)
+ subst; reflexivity.
+ Defined.
+
+ (* holy cow this is ugly *)
+ Definition rcut Γ Δ Σ₃ lev Σ₁₂ :
+ forall Σ₁ Σ₂,
+ ITree Judg judg2exprType [Γ > Δ > Σ₁ |- Σ₁₂ @ lev] ->
+ ITree Judg judg2exprType [Γ > Δ > Σ₁₂ @@@ lev,,Σ₂ |- [Σ₃] @ lev] ->
+ ITree Judg judg2exprType [Γ > Δ > Σ₁,,Σ₂ |- [Σ₃] @ lev].
+
+ induction Σ₁₂.
+ intros.
+ destruct a.
+
+ eapply rlet.
+ apply IBranch.
+ apply X.
+ 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.