First completeness isomorphism theorem done
	modified:   Completeness.agda