Skip to content

Make use of `vec_to_list` coercion in `Forall`/`Forall2` lemmas

Robbert Krebbersrequested to merge
robbert/vec_to_list into master

Unlike commuting lemmas, here there should be no ambiguity.

See discussion in !599 (comment 109974)

Merge request reports