case cons x' xs IH => {
  intros i INBOUND;
  cases i;
  case zero => {
     simp [List.getF];
     constructor;
  }
  case succ i' => {
   simp [List.getF];
   constructor;
   apply IH;
 }
}
α : Type
x' : α
xs : List α
IH : ∀ (i : ℕ) (INBOUND : i < length xs), Mem (getF xs i INBOUND) xs
⊢ ∀ (i : ℕ) (INBOUND : i < length (x' :: xs)), Mem (getF (x' :: xs) i INBOUND) (x' :: xs)
no goals