+ Lemma fresh_lemma Γ ξ vars Σ Σ' lev
+ : Σ = mapOptionTree ξ vars ->
+ FreshM { vars' : _
+ | mapOptionTree (update_ξ(Γ:=Γ) ξ lev ((vars',Σ')::nil)) vars = Σ
+ /\ mapOptionTree (update_ξ ξ lev ((vars',Σ')::nil)) [vars'] = [Σ' @@ lev] }.
+ intros.
+ set (fresh_lemma' Γ [Σ'] vars Σ ξ lev H) as q.
+ refine (q >>>= fun q' => return _).
+ apply FreshMon.
+ clear q.
+ destruct q' as [varstypes [pf1 [pf2 pfdist]]].
+ destruct varstypes; try destruct o; try destruct p; simpl in *.
+ destruct (eqd_dec v v); [ idtac | set (n (refl_equal _)) as n'; inversion n' ].
+ inversion pf2; subst.
+ exists v.
+ destruct (eqd_dec v v); [ idtac | set (n (refl_equal _)) as n'; inversion n' ].
+ split; auto.
+ inversion pf2.
+ inversion pf2.
+ Defined.
+
+ Definition urule2expr : forall Γ Δ h j (r:@URule Γ Δ h j) (ξ:VV -> LeveledHaskType Γ ★),
+ ITree _ (ujudg2exprType ξ) h -> ITree _ (ujudg2exprType ξ) j.
+
+ refine (fix urule2expr Γ Δ h j (r:@URule Γ Δ h j) ξ {struct r} :
+ ITree _ (ujudg2exprType ξ) h -> ITree _ (ujudg2exprType ξ) j :=
+ match r as R in URule H C return ITree _ (ujudg2exprType ξ) H -> ITree _ (ujudg2exprType ξ) C with
+ | RLeft h c ctx r => let case_RLeft := tt in (fun e => _) (urule2expr _ _ _ _ r)
+ | RRight h c ctx r => let case_RRight := tt in (fun e => _) (urule2expr _ _ _ _ r)
+ | RCanL t a => let case_RCanL := tt in _
+ | RCanR t a => let case_RCanR := tt in _
+ | RuCanL t a => let case_RuCanL := tt in _
+ | RuCanR t a => let case_RuCanR := tt in _
+ | RAssoc t a b c => let case_RAssoc := tt in _
+ | RCossa t a b c => let case_RCossa := tt in _
+ | RExch t a b => let case_RExch := tt in _
+ | RWeak t a => let case_RWeak := tt in _
+ | RCont t a => let case_RCont := tt in _
+ end); clear urule2expr; intros.
+
+ destruct case_RCanL.
+ apply ILeaf; simpl; intros.
+ inversion X.
+ simpl in X0.
+ apply (X0 ([],,vars)).
+ simpl; rewrite <- H; auto.
+
+ destruct case_RCanR.
+ apply ILeaf; simpl; intros.
+ inversion X.
+ simpl in X0.
+ apply (X0 (vars,,[])).
+ simpl; rewrite <- H; auto.
+
+ destruct case_RuCanL.
+ apply ILeaf; simpl; intros.
+ destruct vars; try destruct o; inversion H.
+ inversion X.
+ simpl in X0.
+ apply (X0 vars2); auto.
+
+ destruct case_RuCanR.
+ apply ILeaf; simpl; intros.
+ destruct vars; try destruct o; inversion H.
+ inversion X.
+ simpl in X0.
+ apply (X0 vars1); auto.
+
+ destruct case_RAssoc.
+ apply ILeaf; simpl; intros.
+ inversion X.
+ simpl in X0.
+ destruct vars; try destruct o; inversion H.
+ destruct vars1; try destruct o; inversion H.
+ apply (X0 (vars1_1,,(vars1_2,,vars2))).
+ subst; auto.
+
+ destruct case_RCossa.
+ apply ILeaf; simpl; intros.
+ inversion X.
+ simpl in X0.
+ destruct vars; try destruct o; inversion H.
+ destruct vars2; try destruct o; inversion H.
+ apply (X0 ((vars1,,vars2_1),,vars2_2)).
+ subst; auto.
+
+ destruct case_RLeft.
+ destruct c; [ idtac | apply no_urules_with_multiple_conclusions in r0; inversion r0; exists c1; exists c2; auto ].
+ destruct o; [ idtac | apply INone ].
+ destruct u; simpl in *.
+ apply ILeaf; simpl; intros.
+ destruct vars; try destruct o; inversion H.
+ set (fun q => ileaf (e ξ q)) as r'.
+ simpl in r'.
+ apply r' with (vars:=vars2).
+ clear r' e.
+ clear r0.
+ induction h0.
+ destruct a.
+ destruct u.
+ simpl in X.
+ apply ileaf in X.
+ apply ILeaf.
+ simpl.
+ simpl in X.
+ intros.
+ apply X with (vars:=vars1,,vars).
+ simpl.
+ rewrite H0.
+ rewrite H1.
+ reflexivity.
+ apply INone.
+ apply IBranch.
+ apply IHh0_1. inversion X; auto.
+ apply IHh0_2. inversion X; auto.
+ auto.
+
+ destruct case_RRight.
+ destruct c; [ idtac | apply no_urules_with_multiple_conclusions in r0; inversion r0; exists c1; exists c2; auto ].
+ destruct o; [ idtac | apply INone ].
+ destruct u; simpl in *.
+ apply ILeaf; simpl; intros.
+ destruct vars; try destruct o; inversion H.
+ set (fun q => ileaf (e ξ q)) as r'.
+ simpl in r'.
+ apply r' with (vars:=vars1).
+ clear r' e.
+ clear r0.
+ induction h0.
+ destruct a.
+ destruct u.
+ simpl in X.
+ apply ileaf in X.
+ apply ILeaf.
+ simpl.
+ simpl in X.
+ intros.
+ apply X with (vars:=vars,,vars2).
+ simpl.
+ rewrite H0.
+ rewrite H2.
+ reflexivity.
+ apply INone.
+ apply IBranch.
+ apply IHh0_1. inversion X; auto.
+ apply IHh0_2. inversion X; auto.
+ auto.
+
+ destruct case_RExch.
+ apply ILeaf; simpl; intros.
+ inversion X.
+ simpl in X0.
+ destruct vars; try destruct o; inversion H.
+ apply (X0 (vars2,,vars1)).
+ inversion H; subst; auto.
+
+ destruct case_RWeak.
+ apply ILeaf; simpl; intros.
+ inversion X.
+ simpl in X0.
+ apply (X0 []).
+ auto.
+
+ destruct case_RCont.
+ apply ILeaf; simpl; intros.
+ inversion X.
+ simpl in X0.
+ apply (X0 (vars,,vars)).
+ simpl.
+ rewrite <- H.
+ auto.
+ Defined.
+
+ Definition bridge Γ Δ (c:Tree ??(UJudg Γ Δ)) ξ :
+ ITree Judg judg2exprType (mapOptionTree UJudg2judg c) -> ITree (UJudg Γ Δ) (ujudg2exprType ξ) c.
+ intro it.
+ induction c.
+ destruct a.
+ destruct u; simpl in *.
+ apply ileaf in it.
+ apply ILeaf.
+ simpl in *.
+ intros; apply it with (vars:=vars); auto.
+ apply INone.
+ apply IBranch; [ apply IHc1 | apply IHc2 ]; inversion it; auto.
+ Defined.
+
+ 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.