proof for interspersed list length

src/Data/Nat.hs

@@ -129,6 +129,10 @@ succ_right (SS n) m = cong SS (succ_right n m)
 succ_left ∷ Sℕ n → Sℕ m → S (n :+ m) :≡ (S n :+ m)
 succ_left n m = succ_right n m ∾ switch n m
 
+-- | Lemma
+double ∷ Sℕ (S n) -> n :+ n :≡ S (n :+ Pred n)
+double (SS n) = gcastWith (succ_pred (SS n)) (sym (succ_right n (sPred n)))
+
 -- | Relation between successor and addition
 succ_plus ∷ Sℕ n → (n :+ S Z) :≡ S n
 succ_plus n = switch n SZ ∾ plus_right_id (SS n)

src/Data/Vec.hs

@@ -21,7 +21,7 @@ import Relation.Equality (gcastWith, cong, sym)
 import Data.Nat
 import Data.Bool
 import Data.Char         (Char)
-import Data.Function     ((∘))
+import Data.Function     ((∘), ($))
 import Data.TypeClass    (Show, IsList, IsString, Eq) 
 import Data.Singletons   (SingI, sing)
 
@@ -155,8 +155,8 @@ reverse (y :- ys) = gcastWith proof (reverse ys ⧺ (y :- Nil))
 intersperse ∷ a → Vec a n → Vec a (n :+ Pred n)
 intersperse _ Nil        = Nil
 intersperse _ (x :- Nil) = x :- Nil
-intersperse s (x :- xs)  = x :- s :- intersperse s xs
-
+intersperse s (x :- xs)  = gcastWith (double n) (x :- s :- intersperse s xs)
+  where n = sLength (x :- xs)
 
 -- | 'foldl' applied to a binary operator, a starting value
 -- and a 'Vec' reduces the vector to a single value obtained