How does "There" work in the idris tutorial, page 11, section 3.4.4?

Question

Here is the example from the tutorial, slightly modified for simplicity:

data Vect : Nat -> (b:Type) -> Type where
  Nil : Vect Z a
  (::) : a -> Vect k a -> Vect (S k) a

data Elem : a -> Vect n a -> Type where
  Here : {x:a} -> {xs:Vect n a} -> Elem x (x :: xs)
  There : {x,y:a} -> {xs:Vect n a} -> Elem x xs -> Elem x (y :: xs)

testVec : Vect 4 Int
testVec = 3 :: 4 :: 5 :: 6 :: Nil
inVect : Elem 4 testVec
inVect = There Here

I can't understand how There verifies that the value is correct. As far as I understand it, There works like a function, so it takes the element of type Here, which when filling in the holes, corresponds to Elem 3 testVec, then sets the first value of testVec to y, and the rest to xs. But since, y isn't used anywhere, I would except this not to cause any restriction.

However, when I try

inVectBroken : Elem 2 testVec
inVectBroken = There Here

I get an error:

When checking an application of constructor There:
Type mismatch between
        Elem x (x :: xs) (Type of Here)
and
        Elem 2 [4, 5, 6] (Expected type)

Specifically:
        Type mismatch between
                2
        and
                4

Can someone explain to me how the above code works (magically?) to restrict There to the tail of Vect?

Answer 1

Here 4 (x :: xs) is a proof that 4 is at the head of (x :: xs), so x = 4. There takes a proof Elem 4 xs that 4 is somewhere in xs and so proofs Elem 4 (y :: xs), that 4 is still somewhere down a extended list. That is where the y goes to. It does not matter what y actually is, it just allows to extend the proof to larger lists. For example:

in1 : Elem 4 (4 :: Nil)
in1 = Here

in2 : Elem 4 (3 :: 4 :: Nil)
in2 = There in1

in3 : Elem 4 (8 :: 4 :: Nil)
in3 = There in1

By the types you see that not the element 4 changes throughout the proof but the list.