feat(LambdaCalculus): write mapVal in terms of List.map; add similar lemmas

[pepamontero]

This PR adds a lemma mapVal_def showing that mapVal can be written as List.map (Sigma.map id _).

This allows for optimizing the proofs of mapVal_keys and mapVal_mem by using the properties of List.map: map₂_keys and dlookup_map₂.

Other changes:

• I changed the order of mapVal_keys to match map₂_keys (and then I think it can be grind = instead of grind .)

• Since dlookup_map₂ does not exactly coincide with mapVal_mem, I added an additional lemma mapVal_dlookup to match it, and then use this one to prove mapVal_mem (marking it grind).

• Additionally, since NodupKeys.map₂ is just after map₂_keys, I realized a lemma mapVal_wf stating the mapping of values preserves well-formedness could be easily added as well.

• Depends on style(LambdaCalculus): unused variables and other small fixes in Context.lean #918