- 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 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 RCanR ].
+ eapply nd_comp; [ idtac | eapply nd_rule; eapply SFlat; eapply RArrange; eapply RAssoc ].
+ eapply nd_comp; [ idtac | eapply nd_rule; eapply SFlat; eapply RArrange; eapply RLeft; eapply RAssoc ].
+ 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 RComp.
+ eapply RCossa.