Cardano Updates

This pull request adds a proof to `Data.List.Law` that `map` preserves
`isDeduplicated` for injective functions.

```agda
prop-isDeduplicated-map
  : ∀ ⦃ _ : Eq a ⦄ ⦃ _ : IsLawfulEq a ⦄
      ⦃ _ : Eq b ⦄ ⦃ _ : IsLawfulEq b ⦄
  → ∀ (f : a → b) → Injective f
  → ∀ (xs : List a)
  → isDeduplicated xs ≡ True
  → isDeduplicated (map f xs) ≡ True
```

In order to prove this property, it was easier to rework the definition
`isDeduplicated` to be primitively recursive. The previous definition
`isDeduplicated xs = (nub xs == xs)` is now a proven property rather
than a definition.

This pull request adds a module `Data.List` and proves various
properties in `Data.List.Law`.

We are particularly interested in properties of the `nub` function which
removes duplicate elements. This function will be needed to state
properties about the composition `Data.Map.fromAscList ∘
Data.Map.fromList`, as this will remove duplicate keys.

We prove that `nub` is idempotent:

```agda
prop-nub-nub
  : ∀ ⦃ _ : Eq a ⦄ ⦃ _ : IsLawfulEq a ⦄
      (xs : List a)
  → nub (nub xs)
    ≡ nub xs
```