open import Relation.Binary.PropositionalEquality
open import Data.Nat
open import Data.Vec
import Data.Nat.Properties as ℕₚ

data Split {ℓ} {A : Set ℓ} : ∀ {i j} → Vec A i → Vec A (i + j) → Vec A j → Set ℓ where
  l_ : ∀ {i j x l m r} → Split {i = i} {j = j} l m r
     → Split (x ∷ l) (x ∷ m) r
  r_ : ∀ {i j x l m r} → Split {i = i} {j = j} l m r
     → Split l (subst (Vec A) (sym (ℕₚ.+-suc _ _)) (x ∷ m)) (x ∷ r)
  s : Split [] [] []