Proofs simplified. More locale-style specification from Stephan ported.