"Classical" Programming-with-Proofs in lambdaPASym: An Analysis of Non-confluence. - Franco Barbanera; Stefano Berardi; Massimo Schivalocchi (TACS, 1997)