Top Answers

1. How does elim work in Coq on /\ and \/?
   7 votes
2. Using destruct on pattern match expression with 'convoy pattern'
   7 votes
3. Obtain decidable total order on a type from an injection into `nat`
   7 votes
4. coq 8.11.0 incompatible with ocaml 4.10?
   5 votes
5. Tactic automation: simple decision procedure
   4 votes