Start prove of completeness of Propositional Logic

Its soundness is almost proved. There are only some cases left.

Adequacy will take some effort still. The current proof is
nonconstructive, which is a shame (I wanted to use it as a SAT solver),
so I think I will prove it again constructively in the future.

Add default.nix

Refactor and write sketch of get-CNF and get-DNF

Add DNF and CNF definitions, start new proof of Post's Theorem and refactor

The new proof is the one from the book, since I need that particular proof to
prove other theorems.

Begin proof of Post's Theorem

I define truth tables in order to prove Post's Theorem more easily but
get stuck proving the equivalence between tables and functions from
structures to booleans. Apart from that, Post's Theorem is proved, although
with a completely different proof than in the book.

Compile without K

First step to use Cubical Agda

Prove Theorem 3.7.6.b

Prove Theorem 3.7.6.a

Make some parameters explicit

Prove Lemma 3.7.5

Refactor Substitution definition

Previously we needed many implicit arguments to be passed around and
it was annoying. This way there are less. We could also add τ to the
tuple in Substitution and make it have only one argument.

Add substitutions

Added:

- Definition 3.7.1
- Example 3.7.2

Cleanup Lemma 3.6.1

Add until chapter 3.6

Lemma 3.6.1 is not fully proved, since it envolves a lot of boring
machinery, but it will eventually be proved.