+ destruct l as [|ec lev]; simpl.
+ destruct (eqd_dec (g:CoreVar) (hetmet_flatten:CoreVar)).
+ set (garrowfy_code_types (g wev)) as t.
+ set (RGlobal _ Δ nil (mkGlobal Γ t hetmet_id)) as q.
+ simpl in q.
+ apply nd_rule.
+ apply q.
+ apply INil.
+ destruct (eqd_dec (g:CoreVar) (hetmet_unflatten:CoreVar)).
+ set (garrowfy_code_types (g wev)) as t.
+ set (RGlobal _ Δ nil (mkGlobal Γ t hetmet_id)) as q.
+ simpl in q.
+ apply nd_rule.
+ apply q.
+ apply INil.
+ apply nd_rule; rewrite globals_do_not_have_code_types.
+ apply RGlobal.