Generalize Lemma 2.4.2 to dependent functions, close #486