Little steps forward the proof of lift\_2
	modified:   Utilities.agda