ListSet, PropSet, Map helper lemmas

mit-plv / coqutil

Coq library for tactics, basic definitions, sets, maps

MIT License

42 stars 24 forks source link

ListSet, PropSet, Map helper lemmas #110

Closed 0adb closed 7 months ago

0adb commented 8 months ago

Lemmas proved / used for dead code elimination optimization in bedrock2.

0adb commented 7 months ago

I think latest version should have addressed all previous comments. Have removed the too-specific lemma, will make it a helper lemma of DeadCodeElim.v