let isolate y (x, a) = 
  let rec destructure pre post =     (* [pre + post = 0]. *)
    match post with
      | [m] ->
          let (q, y') = mono_of m in
            if Term.eq y y' then
              (pre, q, y, [])
            else 
              raise Not_found
      | m :: post' ->
          let (q, y') = mono_of m in
            if Term.eq y y' then
              (pre, q, y, post')
            else 
              destructure (m :: pre) post'
      | [] ->
          assert false
  in                              (* [pre + q * y + post = a]. *)
  let (pre, q, y, post) = destructure [] (monomials a) in
    assert(not(Q.is_zero q));
    mk_multq (Q.inv q)
      (mk_sub x (mk_addl (pre @ post)))