a way of producing indexes and proofs of inclusion in a GADT Vec, with another GADT maintaining a type level list like [There, Here, There,...]

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