Paulo Emílio de Vilhena issues

Repositories
Issues
Comments

Results 2 issues of


                                            Paulo Emílio de Vilhena

Remove duplicated section.

There are two instances of Section Local Recursive Declarations in induction_and_recursion.md. This pull request removes the second one (at the end of the file).

Add solution to exercise 5.2 from day 1.

Add solution for lemma `set_not_set`. The proof is based on a slightly different version of the lemma `two_equiv_two` that was already proven. Remark: This solution compiles with Coq 8.13.1 and...