+
+ destruct case_SBrak.
+ simpl.
+ destruct lev.
+ drop_simplify.
+ set (drop_lev (ec :: nil) (take_arg_types_as_tree t @@@ (ec :: nil))) as empty_tree.
+ take_simplify.
+ rewrite take_lemma'.
+ simpl.
+ rewrite mapOptionTree_compose.
+ rewrite mapOptionTree_compose.
+ rewrite unlev_relev.
+ rewrite <- mapOptionTree_compose.
+ unfold flatten_leveled_type at 4.
+ simpl.
+ rewrite krunk.
+ set (mapOptionTree flatten_leveled_type (drop_lev (ec :: nil) succ)) as succ_host.
+ set (mapOptionTree (flatten_type ○ unlev)(take_lev (ec :: nil) succ)) as succ_guest.
+ set (mapOptionTree flatten_type (take_arg_types_as_tree t)) as succ_args.
+ unfold empty_tree.
+ eapply nd_comp; [ eapply nd_rule; eapply RArrange; apply tree_of_nothing | idtac ].
+ refine (ga_unkappa' Γ Δ (v2t ec) nil _ _ _ _ ;; _).
+ unfold succ_host.
+ unfold succ_guest.
+ apply arrange_brak.
+ apply (Prelude_error "found Brak at depth >0 indicating 3-level code; only two-level code is currently supported").
+
+ destruct case_SEsc.
+ simpl.
+ destruct lev.
+ simpl.
+ unfold flatten_leveled_type at 2.
+ simpl.
+ rewrite krunk.
+ rewrite mapOptionTree_compose.
+ take_simplify.
+ drop_simplify.
+ simpl.
+ eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply tree_of_nothing' ].
+ simpl.
+ rewrite take_lemma'.
+ rewrite unlev_relev.
+ rewrite <- mapOptionTree_compose.
+ eapply nd_comp; [ apply (arrange_esc _ _ ec) | idtac ].
+
+ set (decide_tree_empty (take_lev (ec :: nil) succ)) as q'.
+ destruct q'.
+ destruct s.
+ rewrite e.
+ clear e.
+
+ set (mapOptionTree flatten_leveled_type (drop_lev (ec :: nil) succ)) as succ_host.
+ set (mapOptionTree flatten_type (take_arg_types_as_tree t)) as succ_args.
+
+ eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply RCanR ].
+ eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ].
+ eapply nd_comp; [ apply nd_llecnac | idtac ].
+ apply nd_prod; [ idtac | eapply boost ].
+ induction x.
+ apply ga_id.
+ eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RCanR ].
+ simpl.
+ apply ga_join.
+ apply IHx1.
+ apply IHx2.
+ simpl.
+ apply postcompose.
+
+ refine ( _ ;; (boost _ _ _ _ _ (postcompose _ _ _ _ _ _ _ _))).
+ apply ga_cancell.
+ apply firstify.
+
+ induction x.
+ destruct a; simpl.
+ apply ga_id.
+ simpl.
+ refine ( _ ;; (boost _ _ _ _ _ (postcompose _ _ _ _ _ _ _ _))).
+ apply ga_cancell.
+ refine ( _ ;; (boost _ _ _ _ _ (postcompose _ _ _ _ _ _ _ _))).
+ eapply firstify.
+ apply IHx1.
+ apply secondify.
+ apply IHx2.
+
+ (* environment has non-empty leaves *)
+ apply ga_kappa'.
+
+ (* nesting too deep *)
+ apply (Prelude_error "found Esc at depth >0 indicating 3-level code; only two-level code is currently supported").