proved the second version of lift\_2->lift
	modified:   PartialMaps.agda
	modified:   Utilities.agda