1 2 3 4 5 6 7 8
mutual _++_⊣_ : (xs ys : UniqList) -> xs ⊄ ys -> UniqList [] ++ ys ⊣ p = ys (x ∷ xs ⊣ q) ++ ys ⊣ p = x ∷ xs ++ ys ⊣ ⊄-next {x} {xs} {q} {ys} p ⊣ (q ⊢++⊣ p x (λ e → proj₁ e PE.refl)) _⊢++⊣_ : ∀ {xs ys i p} -> i ∉ xs -> i ∉ ys -> i ∉ (xs ++ ys ⊣ p) _⊢++⊣_ {[]} q r = r _⊢++⊣_ {x ∷ xs ⊣ o} {ys} {i} {p} (i≠x , i∉xs) i∉ys = i≠x , _⊢++⊣_ {xs} i∉xs i∉ys
