Proof of postulate inserted (with irrelevance issues).
	modified:   Completeness.agda
	modified:   Totals.agda