\begin{code}

module Cons where

open import Mini-library


-- The concatenation maps and some of their properties

cons : {m : ℕ} → ₂Fin m → ₂ℕ → ₂ℕ
cons ⟨⟩      α i        = α i
cons (h ∷ _) α         = h
cons (_ ∷ t) α (succ i) = cons t α i


Lemma[cons-≣_≣] : {n : ℕ} → ∀(s : ₂Fin n) → ∀(α β : ₂ℕ) → cons s α ≣ n ≣ cons s β
Lemma[cons-≣_≣] ⟨⟩      α β i        ()
Lemma[cons-≣_≣] (b ∷ s) α β         r          = refl
Lemma[cons-≣_≣] (b ∷ s) α β (succ i) (≤-succ r) = Lemma[cons-≣_≣] s α β i r

Lemma[cons-take-≣_≣] : ∀(n : ℕ) → ∀(α β : ₂ℕ) → α ≣ n ≣ cons (take n α) β
Lemma[cons-take-≣_≣]         α β i        ()
Lemma[cons-take-≣_≣] (succ n) α β         r          = refl
Lemma[cons-take-≣_≣] (succ n) α β (succ i) (≤-succ r) = Lemma[cons-take-≣_≣] n (α ∘ succ) β i r

Lemma[cons-take-drop] : ∀(n : ℕ) → ∀(α : ₂ℕ) →
                         ∀(i : ℕ) → cons (take n α) (drop n α) i ≡ α i
Lemma[cons-take-drop]         α i        = refl
Lemma[cons-take-drop] (succ n) α         = refl
Lemma[cons-take-drop] (succ n) α (succ i) = Lemma[cons-take-drop] n (α ∘ succ) i


Lemma[cons-drop] : ∀(n : ℕ) → ∀(α : ₂ℕ) → ∀(i : ℕ) → drop n α i ≡ α (i + n)
Lemma[cons-drop]         α i = refl
Lemma[cons-drop] (succ n) α i = Lemma[cons-drop] n (α ∘ succ) i


Lemma[cons-UC] : ∀{n : ℕ} → ∀(s : ₂Fin n) → uniformly-continuous-₂ℕ (cons s)
Lemma[cons-UC] ⟨⟩      m        = ∃-intro m (λ α β z → z)
Lemma[cons-UC] (b ∷ s)         = ∃-intro  (λ α β _ i → λ ())
Lemma[cons-UC] (b ∷ s) (succ m) = ∃-intro k prf
 where
  k : ℕ
  k = ∃-witness (Lemma[cons-UC] s m)
  prf : ∀(α β : ₂ℕ) → α ≣ k ≣ β →
         ∀(i : ℕ) → i < succ m → cons (b ∷ s) α i ≡ cons (b ∷ s) β i
  prf α β aw         r          = refl
  prf α β aw (succ i) (≤-succ r) = ∃-elim (Lemma[cons-UC] s m) α β aw i r

\end{code}