Skip to main content
5 votes
Accepted

How to implement first-order relational structures in Coq?

Supplemental: It looks like I misunderstood the point of the question and the OP might have simply been looking for the sig type, usually written as ...
Andrej Bauer's user avatar
  • 9,104
3 votes

How to unfold definitions in Lean / find the right theorems to apply?

After quite a bit of searching, I did find a number of things to try that seem to cover most of what I need here: ...
Pieter Cuijpers's user avatar
2 votes
Accepted

Assistance using destruct on an equality proof for functors

Solution 1. Use UIP (Uniqueness of Identity Proofs). ...
Li-yao Xia's user avatar
  • 1,757

Only top scored, non community-wiki answers of a minimum length are eligible