Soundness is done.
	modified:   Soundness.agda