added EM2
	new file:   EM2.agda
	modified:   Equality.agda
	modified:   Everything.agda