Two independent topics are treated. First, the problem of weakening/strengthening steps in calculational proofs is discussed and a form of substantiating such steps is proposed. Second, a simple proof of (Ex| R.x: (Ay| S.y: P.x.y)) greater than or equal to (Ay| S.y: (Ex| R.x: P.x.y)) is presented, which uses the idea of a witness for an existnetial quantification.