induction xs
α : Type
xs : List α
⊢ ∀ (i : ℕ) (INBOUND : i < length xs), Mem (getF xs i INBOUND) xs
case nil
α : Type
⊢ ∀ (i : ℕ) (INBOUND : i < length []), Mem (getF [] i INBOUND) []

case cons
α : Type
head✝ : α
tail✝ : List α
tail_ih✝ : ∀ (i : ℕ) (INBOUND : i < length tail✝), Mem (getF tail✝ i INBOUND) tail✝
⊢ ∀ (i : ℕ) (INBOUND : i < length (head✝ :: tail✝)), Mem (getF (head✝ :: tail✝) i INBOUND) (head✝ :: tail✝)