+ unfold flatten_leveled_type at 3.
+ simpl.
+ apply nd_rule.
+ set (@RLetRec Γ Δ (mapOptionTree flatten_leveled_type lri) (flatten_type x) (mapOptionTree flatten_type y) nil) as q.
+ simpl in q.
+ apply q.
+ induction y; try destruct a; auto.
+ simpl.
+ rewrite IHy1.
+ rewrite IHy2.
+ reflexivity.
+ induction y; try destruct a; auto.
+ simpl.
+ rewrite <- IHy1.
+ rewrite <- IHy2.
+ reflexivity.
+ apply (Prelude_error "LetRec not supported inside brackets yet (FIXME)").