- destruct case_RLet.
- simpl.
- destruct lev as [|ec lev]; simpl; [ apply nd_rule; apply RLet; auto | idtac ].
- repeat drop_simplify.
- repeat take_simplify.
- simpl.
-
- set (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) Σ₁)) as Σ₁'.
- set (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) Σ₂)) as Σ₂'.
- set (mapOptionTree flatten_leveled_type (drop_lev (ec :: lev) Σ₁)) as Σ₁''.
- set (mapOptionTree flatten_leveled_type (drop_lev (ec :: lev) Σ₂)) as Σ₂''.
-
- eapply nd_comp.
- eapply nd_prod; [ idtac | apply nd_id ].
- eapply boost.
- apply (ga_first _ _ _ _ _ _ Σ₂').
-
- eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ].
- apply nd_prod.
- apply nd_id.
- eapply nd_comp; [ eapply nd_rule; eapply RArrange; eapply ACanL | idtac ].
- eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply AExch (* okay *)].
- apply precompose.
-
- destruct case_RWhere.
- simpl.
- destruct lev as [|ec lev]; simpl; [ apply nd_rule; apply RWhere; auto | idtac ].
- repeat take_simplify.
- repeat drop_simplify.
- simpl.
-
- set (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) Σ₁)) as Σ₁'.
- set (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) Σ₂)) as Σ₂'.
- set (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) Σ₃)) as Σ₃'.
- set (mapOptionTree flatten_leveled_type (drop_lev (ec :: lev) Σ₁)) as Σ₁''.
- set (mapOptionTree flatten_leveled_type (drop_lev (ec :: lev) Σ₂)) as Σ₂''.
- set (mapOptionTree flatten_leveled_type (drop_lev (ec :: lev) Σ₃)) as Σ₃''.
-
- eapply nd_comp.
- eapply nd_prod; [ eapply nd_id | idtac ].
- eapply (first_nd _ _ _ _ _ _ Σ₃').
- eapply nd_comp.
- eapply nd_prod; [ eapply nd_id | idtac ].
- eapply (second_nd _ _ _ _ _ _ Σ₁').
-
- eapply nd_comp; [ idtac | eapply nd_rule; eapply RWhere ].
- apply nd_prod; [ idtac | apply nd_id ].
- eapply nd_comp; [ idtac | eapply precompose' ].
- apply nd_rule.
- apply RArrange.
- apply ALeft.
- apply ACanL.
-