- apply RArrange.
- apply RCanR.
- eapply nd_comp; [ eapply nd_rule; apply SFlat; eapply RArrange; apply RCossa | idtac ].
- eapply nd_comp; [ idtac | eapply nd_rule; apply SFlat; eapply RArrange; apply RAssoc ].
- apply nd_rule.
- apply SFlat.
- apply RArrange.
- apply RLeft.
- eapply RExch.
+ apply RWhere.
+ set (check_hof σ₁) as hof_tx.
+ destruct hof_tx; [ apply (Prelude_error "attempt to let-bind a higher-order function at depth>0") | idtac ].
+ destruct a.
+ rewrite H.
+ rewrite H0.
+
+ eapply nd_comp.
+ eapply nd_prod; [ apply nd_id | eapply nd_rule; eapply SFlat; eapply RArrange; eapply ACanR ].
+ eapply nd_comp; [ idtac | eapply nd_rule; eapply SFlat; eapply RArrange; eapply AAssoc ].
+ eapply nd_comp; [ idtac | eapply nd_rule; eapply SFlat; eapply RArrange; eapply ALeft; eapply AAssoc ].
+ eapply nd_comp; [ idtac | eapply nd_rule; eapply SFlat; eapply RWhere ].
+ apply nd_prod; [ idtac | eapply nd_id ].
+ eapply nd_rule; apply SFlat; eapply RArrange.
+ eapply AComp.
+ eapply AuAssoc.
+ apply ALeft.
+ eapply AuAssoc.