spec    proof comments
        3        0        2 coqwc/BZ5756.v