```------------------------------------------------------------------------
-- Some boring lemmas
------------------------------------------------------------------------

module StructurallyRecursiveDescentParsing.Simplified.Lemmas where

open import Algebra
open import Data.Product
open import Function
open import Level

import Data.List.NonEmpty as List⁺
open List⁺ using (List⁺; _∷_; [_]; _⁺++⁺_; head; tail)
using () renaming (_>>=_ to _>>=⁺_)
open import Data.List.NonEmpty.Properties

import Data.List as List
open List using (List; _∷_; []; _++_)
private module LM {A : Set} = Monoid (List.monoid A)
using () renaming (_>>=_ to _>>=′_)
import Data.List.Properties as ListProp

open import Relation.Binary.PropositionalEquality
open ≡-Reasoning

tail-++ : {A : Set} (xs ys : List⁺ A) →
tail xs ++ List⁺.toList ys ≡ tail (xs ⁺++⁺ ys)
tail-++ [ x ]    ys = refl
tail-++ (x ∷ xs) ys = toList-⁺++⁺ xs ys

head->>= : {A B : Set} (f : A → List⁺ B) (xs : List⁺ A) →
head->>= f [ x ]    = refl
head->>= f (x ∷ xs) with f x
head->>= f (x ∷ xs) | [ y ]    = refl
head->>= f (x ∷ xs) | (y ∷ ys) = refl

tail->>= : {A B : Set} (f : A → List⁺ B) (xs : List⁺ A) →
tail (f (head xs)) ++ (tail xs >>=′ λ x → head (f x) ∷ tail (f x)) ≡
tail (xs >>=⁺ f)
tail->>= f [ x ]    = proj₂ LM.identity _
tail->>= f (x ∷ xs) = begin
tail (f x) ++ (List⁺.toList xs >>=′ λ x → head (f x) ∷ tail (f x)) ≡⟨ cong (λ ys → tail (f x) ++ List.concat ys)
(ListProp.map-cong (η ∘ f) (List⁺.toList xs)) ⟩
tail (f x) ++ (List⁺.toList xs >>=′ List⁺.toList ∘ f)              ≡⟨ cong (_++_ (tail (f x))) (toList->>= f xs) ⟩
tail (f x) ++ (List⁺.toList (xs >>=⁺ f))                           ≡⟨ tail-++ (f x) (xs >>=⁺ f) ⟩
tail (f x ⁺++⁺ (xs >>=⁺ f))                                        ≡⟨ refl ⟩
tail (x ∷ xs >>=⁺ f)                                               ∎
```