I was just searching for this lemma for at least 5 minutes until I realized that this is the definition of map_Forall -- usually our definitions are such that just Printing stuff doesn't actually get me anywhere useful.
I think it would be good for a lemma like this to show up in Search results.