no goals
α : Type u_1
i : Nat
as bs : List α
h : i < length as
h' : i < length (as ++ bs)
⊢ get (as ++ bs) { val := i, isLt := h' } = get as { val := i, isLt := h }
induction as generalizing i with
| nil => trivial
| cons a as ih =>
  cases i with
  | zero => rfl
  | succ i => apply ih
no goals
case nil
α : Type u_1
bs : List α
i : Nat
h : i < length []
h' : i < length ([] ++ bs)
⊢ get ([] ++ bs) { val := i, isLt := h' } = get [] { val := i, isLt := h }
trivial
no goals
case cons
α : Type u_1
bs : List α
a : α
as : List α
ih :
  ∀ {i : Nat} (h : i < length as) {h' : i < length (as ++ bs)},
    get (as ++ bs) { val := i, isLt := h' } = get as { val := i, isLt := h }
i : Nat
h : i < length (a :: as)
h' : i < length (a :: as ++ bs)
⊢ get (a :: as ++ bs) { val := i, isLt := h' } = get (a :: as) { val := i, isLt := h }
cases i with
| zero => rfl
| succ i => apply ih
no goals
case cons.zero
α : Type u_1
bs : List α
a : α
as : List α
ih :
  ∀ {i : Nat} (h : i < length as) {h' : i < length (as ++ bs)},
    get (as ++ bs) { val := i, isLt := h' } = get as { val := i, isLt := h }
h : Nat.zero < length (a :: as)
h' : Nat.zero < length (a :: as ++ bs)
⊢ get (a :: as ++ bs) { val := Nat.zero, isLt := h' } = get (a :: as) { val := Nat.zero, isLt := h }
rfl
no goals
case cons.succ
α : Type u_1
bs : List α
a : α
as : List α
ih :
  ∀ {i : Nat} (h : i < length as) {h' : i < length (as ++ bs)},
    get (as ++ bs) { val := i, isLt := h' } = get as { val := i, isLt := h }
i : Nat
h : Nat.succ i < length (a :: as)
h' : Nat.succ i < length (a :: as ++ bs)
⊢ get (a :: as ++ bs) { val := Nat.succ i, isLt := h' } = get (a :: as) { val := Nat.succ i, isLt := h }
apply ih