comments
	modified:   Delay.agda
proved lookupLev≤-•

two implcit args (x and i) were different for lookupSuc so couldn't use hcong directly, I tried using hcong\_3 but too much stuff implicit stuff needed to be supplied, so created a lemma for proving lookupSuc l \cong lookupSuc l'.

	modified:   DBLevel.agda
	modified:   Library.agda