Checking confluence of rewrite rules.

Given a rewrite rule f ps ↦ v, we construct critical pairs involving this as the main rule by searching for:

1. *Different* rules f ps' ↦ v' where ps and ps' can be unified@.
2. Subpatterns g qs of ps and rewrite rules g qs' ↦ w where qs and qs' can be unified.

Each of these leads to a *critical pair* v₁ u -- v₂, which should satisfy v₁ = v₂.