Prove properties about HList in idris2, specifically: length (some_lhs ++ [elem] ++ some_rhs) = length original

Question

I have trouble proving facts about appends on HList. I've written a function that breaks down a HList into ls ++ [x] ++ rs for some ls, rs, provided with the proof that x:ty is an element of given HList:

triplet : {x : ty} -> {p : Nat} -> {tps : Vect (S p) Type} -> {list : HList (S p) tps} -> (1 pf : Elem x list) -> 
    (k ** n ** ls : Vect k _ ** rs : Vect n _ ** HList _ (ls ++ [ty] ++ rs))
triplet Here {list = x :: xs} {tps = ty :: ties} = (0 ** p ** [] ** ties ** x :: xs)
triplet (There has) {list = x :: xs} {tps = ty :: ties} = let (k ** n ** ls ** rs ** list) = triplet has in 
          (1 + k ** n ** ty :: ls ** rs ** x :: list)              

Now I want to prove that length of triplet of any list is the same as the length of the input list:

tripletLenSum : {x : ty} -> {p : Nat} -> {tps : Vect (S p) Type} -> {list : HList (S p) tps} -> (pf : Elem x list) ->
      (let (k ** n ** _) = triplet pf in p = k + n)
tripletLenSum Here = Refl
tripletLenSum (There there) {p = S q} {tps = ty1 :: ties} {list = el :: els} = ?proof_please 

I tried 100 times and failed 100 times... The main culprit as I see it is dependent typing in the return type of tripletLenSum:

let (k ** n ** _) = triplet pf in p = k + n

Type of ?proof_please is

0 ty : Type
   x : ty
   q : Nat
   ty1 : Type
   ties : Vect (S q) Type
   el : ty1
   els : HList (S q) ties
   there : Elem x els
-------------------------------------
proof_please : case case triplet there of { MkDPair k (MkDPair n (MkDPair ls (MkDPair rs list))) => MkDPair (S k) (MkDPair n (MkDPair (ty :: ls) (MkDPair rs (x :: list)))) } of { MkDPair k (MkDPair n _) => p = k + n }

With clauses helped a little in some attempts but not much. Case clauses weren't able to break that case type...

Help ?

Complete runnable code (Idris2)