Martin Simons, Michel Sintzoff: Algebraic Composition and Refinement of Proofs. AMAST 1997: 494-508