Add solution to exercise 5.2 from day 1.

[DeVilhena-Paulo]

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 Coq-HoTT 8.13.