simp [List.getF]
α : Type
x' : α
xs : List α
IH : ∀ (i : ℕ) (INBOUND : i < length xs), Mem (getF xs i INBOUND) xs
INBOUND : Nat.zero < length (x' :: xs)
⊢ Mem (getF (x' :: xs) Nat.zero INBOUND) (x' :: xs)
α : Type
x' : α
xs : List α
IH : ∀ (i : ℕ) (INBOUND : i < length xs), Mem (getF xs i INBOUND) xs
INBOUND : Nat.zero < length (x' :: xs)
⊢ Mem x' (x' :: xs)