Actually show the bij_betw lemma