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