proved lvl≤-• up to h-eq. added hcong\_3 to the Library.
	modified:   DBLevel.agda
	modified:   Library.agda