add map_Forall_lookup

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.

Such a lemma makes sense. Note that Forall_lookup for lists is an iff, and we have lemmas _1 and _2 for both directions.

added 1 commit

• a6d4d077 - prove lemma in both directions

Compare with previous version

LGTM.

merged

mentioned in commit fb90d2d8