rename lemma-from-just to just-injective