fixed completeness
modified:   Completeness.agda