switched from let to where and improved a few proofs
	modified:   Adjunctions/Adj2Mon.agda
	modified:   RMonads/Restriction.agda
	modified:   RMonads/SpecialCase.agda