move lemma-just!=nothing to FinMap and use it there