Skip to content

remove some lemmas that exist in Coq's stdlib

Ralf Jung requested to merge ralf/qc into master

These lemmas were added in https://github.com/coq/coq/commit/ea05377f19404e0627a105b07c10ce72fb010af9, which was included in Coq 8.6. Time to remove our copies of them. :)

Merge request reports

Loading