you use them to prove a certain element is at a certain position in a Vec, therefore that it is present. You can also provide a proof that the Here There list has only one Here, proving uniqueness

There means there's an instance of the element somewhere after this position. when the list ends earlier that means theres no more, so a non included element is just proven by an empty Here There list