Skip to content

add map_Forall_lookup

Ralf Jung requested to merge ralf/map-forall-lookup into master

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.

Merge request reports