All Questions
2
questions
1
vote
1
answer
128
views
Rewriting inside quantified propositions in Coq?
Is there a simple way to use rewrites inside quantified Props? As an example, consider the following:
...
- 1,502
2
votes
1
answer
154
views
Debug autorewrite in Coq
I often meet proofs using autorewrite which Coq takes a while to process for some reason. (Setoid rewriting)
I then manually figure out which rewrite rules were ...
- 224