module GeneralLemmas where
open import Data.Empty
  public using (; ⊥-elim)
open import Data.List
  public using (List; _∷_; []; _++_; length; map)
open import Data.Maybe
  public using (Maybe; just; nothing)
open import Data.Product
  public using (_×_; _,_; proj₁; proj₂;; ∃₂)
open import Data.Nat
  public using (; suc; zero; _+_; _≤_; z≤n; s≤s)
open import Data.Nat.Properties
  public using (≤-steps)
open import Data.Unit
  public using (; tt)
open import Function
  public using (_∋_; _∘_; id)
open import Relation.Binary
open DecTotalOrder Data.Nat.decTotalOrder public using () renaming (refl to ≤-refl)
open import Relation.Binary.PropositionalEquality
  public using (_≡_; _≢_; refl; cong; cong₂; subst; subst₂; trans; sym; inspect; [_])
open import Relation.Nullary
  public using (Dec; yes; no; ¬_)

,-inj : {A B : Set}{x y : A × B}
       x  y  proj₁ x  proj₁ y × proj₂ x  proj₂ y
,-inj refl = refl , refl

,,-inj : {A B C : Set}{x y : A × B × C}  x  y
        proj₁ x  proj₁ y × proj₁ (proj₂ x)  proj₁ (proj₂ y) × proj₂ (proj₂ x)  proj₂ (proj₂ y)
,,-inj refl = refl , refl , refl

∷-inj : {A : Set}{x y : A}{xs ys : List A}  (List A  x  xs)  y  ys  x  y × xs  ys
∷-inj refl = refl , refl

just-inj : {A : Set}{x y : A}  (Maybe A  just x)  just y  x  y
just-inj refl = refl

nothing≠just :  {A : Set}{x : A}  nothing  (Maybe A  just x)
nothing≠just ()

cong₄ :  {a b c d e} {A : Set a} {B : Set b} {C : Set c} {D : Set d} {E : Set e}
        (f : A  B  C  D  E) {w w' x x' y y' z z'}
         w  w'  x  x'  y  y'  z  z'  f w x y z  f w' x' y' z'
cong₄ f refl refl refl refl = refl

cong₃ :  {a b c d} {A : Set a} {B : Set b} {C : Set c} {D : Set d}
        (f : A  B  C  D) {w w' x x' y y'}
         w  w'  x  x'  y  y'  f w x y  f w' x' y'
cong₃ f refl refl refl = refl

lookup : {A : Set}    List A  Maybe A
lookup n [] = nothing
lookup zero (x  xs) = just x
lookup (suc n) (x  xs) = lookup n xs