Added "opt" lemma and moved OSR to right place