Module Serlib.Ser_proof