have the iso for the congruence proof. Triangles remain.
congruence proof done.
	modified:   PartialMaps.agda