This adds a function to enumerate all vectors of a given type and a helper lemma about NoDup and bind.
@robbertkrebbers Can vec_finite be used to simplify the proof of list_finite?
vec_finite
list_finite
00:17:51
2 years ago
No artifacts found
00:02:44
