Add `list_diff_length` lemma to coqutil

mit-plv / coqutil

Coq library for tactics, basic definitions, sets, maps

MIT License

42 stars 24 forks source link

Closed pratapsingh1729 closed 2 years ago

pratapsingh1729 commented 2 years ago

This lemma is needed for the metrics proofs in the bedrock2 FlatToRiscvFunctions pass.