moving forward the proof of the completeness theorem
	modified:   Completeness.agda