+ Definition judges2exprType (j:Tree ??Judg) : Type :=
+ ITree _ judg2exprType j.
+
+ Definition urule2expr Γ Δ : forall h j (r:@URule Γ Δ h j),
+ judges2exprType (mapOptionTree UJudg2judg h) -> judges2exprType (mapOptionTree UJudg2judg j).
+
+ intros h j r.
+
+ refine (match r as R in URule H C
+ return judges2exprType (mapOptionTree UJudg2judg H) -> judges2exprType (mapOptionTree UJudg2judg C) with
+ | RLeft h c ctx r => let case_RLeft := tt in _
+ | RRight h c ctx r => let case_RRight := tt in _
+ | 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 ); 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.
+ (* this will require recursion *)
+ admit.
+
+ destruct case_RRight.
+ (* this will require recursion *)
+ admit.
+
+ 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 rule2expr : forall h j (r:Rule h j), judges2exprType h -> judges2exprType j.
+
+ intros h j r.
+
+ refine (match r as R in Rule H C return judges2exprType H -> judges2exprType C with