Proved soundness with new quotients.
	modified:   Soundness.agda