renamed lookupSucLem to lookupSucCong
lvl-leq-bullet can be in homogeneous equality in the end