let rec on_computation w =
  match w with
  | Var c -> Some c, one
  | Pbw p -> None, p
  | On (w1, w2) ->
      let c1_opt, p1 = on_computation w1 in
      let c2_opt, p2 = on_computation w2 in
      assert (c2_opt = None);
      c1_opt, on p1 p2