equational proofs and better use of modules
	modified:   RKleisliAdj2.agda
	modified:   RKleisliFunctors2.agda
	modified:   Restriction.agda
	modified:   SpecialCase.agda