| Qed _ -> a
| Branch (pps, _) -> List.fold_left count_steps a pps
| _ -> succ a
and count_steps a = List.fold_left count_step a
| Qed _ -> a
| Branch (pps, _) -> List.fold_left count_steps a pps
| _ -> succ a
and count_steps a = List.fold_left count_step a