α : Type u_1
β : Type ?u.254009
γ : Type ?u.254012
σ : Type ?u.254015
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
F : List α → ℕ → ℕ ⊕ α :=
  fun l n => List.foldl (fun s a => Sum.casesOn s (fun x => Nat.casesOn x (Sum.inr a) Sum.inl) Sum.inr) (Sum.inl n) l
hF : Primrec₂ F
this : Primrec fun p => Sum.casesOn (F p.fst p.snd) (fun x => none) some
l : List α
n : ℕ
⊢ Sum.rec (fun val => none) (fun val => some val)
      (List.foldl
        (fun s a => Sum.rec (fun val => Nat.rec (Sum.inr a) (fun n n_ih => Sum.inl n) val) (fun val => Sum.inr val) s)
        (Sum.inl n) l) =
    List.get? l n
α : Type u_1
β : Type ?u.254009
γ : Type ?u.254012
σ : Type ?u.254015
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
F : List α → ℕ → ℕ ⊕ α :=
  fun l n => List.foldl (fun s a => Sum.casesOn s (fun x => Nat.casesOn x (Sum.inr a) Sum.inl) Sum.inr) (Sum.inl n) l
hF : Primrec₂ F
this : Primrec fun p => Sum.casesOn (F p.fst p.snd) (fun x => none) some
l : List α
n : ℕ
⊢ Sum.casesOn (F (l, n).fst (l, n).snd) (fun x => none) some = List.get? l n
dsimp
α : Type u_1
β : Type ?u.254009
γ : Type ?u.254012
σ : Type ?u.254015
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
F : List α → ℕ → ℕ ⊕ α :=
  fun l n => List.foldl (fun s a => Sum.casesOn s (fun x => Nat.casesOn x (Sum.inr a) Sum.inl) Sum.inr) (Sum.inl n) l
hF : Primrec₂ F
this : Primrec fun p => Sum.casesOn (F p.fst p.snd) (fun x => none) some
l : List α
n : ℕ
⊢ List.get? l n =
    Sum.rec (fun val => none) (fun val => some val)
      (List.foldl
        (fun s a => Sum.rec (fun val => Nat.rec (Sum.inr a) (fun n n_ih => Sum.inl n) val) (fun val => Sum.inr val) s)
        (Sum.inl n) l)
α : Type u_1
β : Type ?u.254009
γ : Type ?u.254012
σ : Type ?u.254015
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
F : List α → ℕ → ℕ ⊕ α :=
  fun l n => List.foldl (fun s a => Sum.casesOn s (fun x => Nat.casesOn x (Sum.inr a) Sum.inl) Sum.inr) (Sum.inl n) l
hF : Primrec₂ F
this : Primrec fun p => Sum.casesOn (F p.fst p.snd) (fun x => none) some
l : List α
n : ℕ
⊢ Sum.rec (fun val => none) (fun val => some val)
      (List.foldl
        (fun s a => Sum.rec (fun val => Nat.rec (Sum.inr a) (fun n n_ih => Sum.inl n) val) (fun val => Sum.inr val) s)
        (Sum.inl n) l) =
    List.get? l n
symm
case nil
α : Type u_1
β : Type ?u.254009
γ : Type ?u.254012
σ : Type ?u.254015
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
F : List α → ℕ → ℕ ⊕ α :=
  fun l n => List.foldl (fun s a => Sum.casesOn s (fun x => Nat.casesOn x (Sum.inr a) Sum.inl) Sum.inr) (Sum.inl n) l
hF : Primrec₂ F
this : Primrec fun p => Sum.casesOn (F p.fst p.snd) (fun x => none) some
n✝ n : ℕ
⊢ List.get? [] n =
    Sum.rec (fun val => none) (fun val => some val)
      (List.foldl
        (fun s a => Sum.rec (fun val => Nat.rec (Sum.inr a) (fun n n_ih => Sum.inl n) val) (fun val => Sum.inr val) s)
        (Sum.inl n) [])

case cons
α : Type u_1
β : Type ?u.254009
γ : Type ?u.254012
σ : Type ?u.254015
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
F : List α → ℕ → ℕ ⊕ α :=
  fun l n => List.foldl (fun s a => Sum.casesOn s (fun x => Nat.casesOn x (Sum.inr a) Sum.inl) Sum.inr) (Sum.inl n) l
hF : Primrec₂ F
this : Primrec fun p => Sum.casesOn (F p.fst p.snd) (fun x => none) some
n✝ : ℕ
a : α
l : List α
IH :
  ∀ (n : ℕ),
    List.get? l n =
      Sum.rec (fun val => none) (fun val => some val)
        (List.foldl
          (fun s a => Sum.rec (fun val => Nat.rec (Sum.inr a) (fun n n_ih => Sum.inl n) val) (fun val => Sum.inr val) s)
          (Sum.inl n) l)
n : ℕ
⊢ List.get? (a :: l) n =
    Sum.rec (fun val => none) (fun val => some val)
      (List.foldl
        (fun s a => Sum.rec (fun val => Nat.rec (Sum.inr a) (fun n n_ih => Sum.inl n) val) (fun val => Sum.inr val) s)
        (Sum.inl n) (a :: l))
α : Type u_1
β : Type ?u.254009
γ : Type ?u.254012
σ : Type ?u.254015
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
F : List α → ℕ → ℕ ⊕ α :=
  fun l n => List.foldl (fun s a => Sum.casesOn s (fun x => Nat.casesOn x (Sum.inr a) Sum.inl) Sum.inr) (Sum.inl n) l
hF : Primrec₂ F
this : Primrec fun p => Sum.casesOn (F p.fst p.snd) (fun x => none) some
l : List α
n : ℕ
⊢ List.get? l n =
    Sum.rec (fun val => none) (fun val => some val)
      (List.foldl
        (fun s a => Sum.rec (fun val => Nat.rec (Sum.inr a) (fun n n_ih => Sum.inl n) val) (fun val => Sum.inr val) s)
        (Sum.inl n) l)
induction' l with a l IH generalizing n
case cons.zero
α : Type u_1
β : Type ?u.254009
γ : Type ?u.254012
σ : Type ?u.254015
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
F : List α → ℕ → ℕ ⊕ α :=
  fun l n => List.foldl (fun s a => Sum.casesOn s (fun x => Nat.casesOn x (Sum.inr a) Sum.inl) Sum.inr) (Sum.inl n) l
hF : Primrec₂ F
this : Primrec fun p => Sum.casesOn (F p.fst p.snd) (fun x => none) some
n : ℕ
a : α
l : List α
IH :
  ∀ (n : ℕ),
    List.get? l n =
      Sum.rec (fun val => none) (fun val => some val)
        (List.foldl
          (fun s a => Sum.rec (fun val => Nat.rec (Sum.inr a) (fun n n_ih => Sum.inl n) val) (fun val => Sum.inr val) s)
          (Sum.inl n) l)
⊢ List.get? (a :: l) Nat.zero =
    Sum.rec (fun val => none) (fun val => some val)
      (List.foldl
        (fun s a => Sum.rec (fun val => Nat.rec (Sum.inr a) (fun n n_ih => Sum.inl n) val) (fun val => Sum.inr val) s)
        (Sum.inl Nat.zero) (a :: l))

case cons.succ
α : Type u_1
β : Type ?u.254009
γ : Type ?u.254012
σ : Type ?u.254015
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
F : List α → ℕ → ℕ ⊕ α :=
  fun l n => List.foldl (fun s a => Sum.casesOn s (fun x => Nat.casesOn x (Sum.inr a) Sum.inl) Sum.inr) (Sum.inl n) l
hF : Primrec₂ F
this : Primrec fun p => Sum.casesOn (F p.fst p.snd) (fun x => none) some
n✝ : ℕ
a : α
l : List α
IH :
  ∀ (n : ℕ),
    List.get? l n =
      Sum.rec (fun val => none) (fun val => some val)
        (List.foldl
          (fun s a => Sum.rec (fun val => Nat.rec (Sum.inr a) (fun n n_ih => Sum.inl n) val) (fun val => Sum.inr val) s)
          (Sum.inl n) l)
n : ℕ
⊢ List.get? (a :: l) (Nat.succ n) =
    Sum.rec (fun val => none) (fun val => some val)
      (List.foldl
        (fun s a => Sum.rec (fun val => Nat.rec (Sum.inr a) (fun n n_ih => Sum.inl n) val) (fun val => Sum.inr val) s)
        (Sum.inl (Nat.succ n)) (a :: l))
case cons
α : Type u_1
β : Type ?u.254009
γ : Type ?u.254012
σ : Type ?u.254015
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
F : List α → ℕ → ℕ ⊕ α :=
  fun l n => List.foldl (fun s a => Sum.casesOn s (fun x => Nat.casesOn x (Sum.inr a) Sum.inl) Sum.inr) (Sum.inl n) l
hF : Primrec₂ F
this : Primrec fun p => Sum.casesOn (F p.fst p.snd) (fun x => none) some
n✝ : ℕ
a : α
l : List α
IH :
  ∀ (n : ℕ),
    List.get? l n =
      Sum.rec (fun val => none) (fun val => some val)
        (List.foldl
          (fun s a => Sum.rec (fun val => Nat.rec (Sum.inr a) (fun n n_ih => Sum.inl n) val) (fun val => Sum.inr val) s)
          (Sum.inl n) l)
n : ℕ
⊢ List.get? (a :: l) n =
    Sum.rec (fun val => none) (fun val => some val)
      (List.foldl
        (fun s a => Sum.rec (fun val => Nat.rec (Sum.inr a) (fun n n_ih => Sum.inl n) val) (fun val => Sum.inr val) s)
        (Sum.inl n) (a :: l))
cases' n with n
no goals
case nil
α : Type u_1
β : Type ?u.254009
γ : Type ?u.254012
σ : Type ?u.254015
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
F : List α → ℕ → ℕ ⊕ α :=
  fun l n => List.foldl (fun s a => Sum.casesOn s (fun x => Nat.casesOn x (Sum.inr a) Sum.inl) Sum.inr) (Sum.inl n) l
hF : Primrec₂ F
this : Primrec fun p => Sum.casesOn (F p.fst p.snd) (fun x => none) some
n✝ n : ℕ
⊢ List.get? [] n =
    Sum.rec (fun val => none) (fun val => some val)
      (List.foldl
        (fun s a => Sum.rec (fun val => Nat.rec (Sum.inr a) (fun n n_ih => Sum.inl n) val) (fun val => Sum.inr val) s)
        (Sum.inl n) [])
rfl
case cons.zero
α : Type u_1
β : Type ?u.254009
γ : Type ?u.254012
σ : Type ?u.254015
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
F : List α → ℕ → ℕ ⊕ α :=
  fun l n => List.foldl (fun s a => Sum.casesOn s (fun x => Nat.casesOn x (Sum.inr a) Sum.inl) Sum.inr) (Sum.inl n) l
hF : Primrec₂ F
this : Primrec fun p => Sum.casesOn (F p.fst p.snd) (fun x => none) some
n : ℕ
a : α
l : List α
IH :
  ∀ (n : ℕ),
    List.get? l n =
      Sum.rec (fun val => none) (fun val => some val)
        (List.foldl
          (fun s a => Sum.rec (fun val => Nat.rec (Sum.inr a) (fun n n_ih => Sum.inl n) val) (fun val => Sum.inr val) s)
          (Sum.inl n) l)
⊢ some a =
    Sum.rec (fun val => none) (fun val => some val)
      (List.foldl
        (fun s a => Sum.rec (fun val => Nat.rec (Sum.inr a) (fun n n_ih => Sum.inl n) val) (fun val => Sum.inr val) s)
        (Sum.inr a) l)
case cons.zero
α : Type u_1
β : Type ?u.254009
γ : Type ?u.254012
σ : Type ?u.254015
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
F : List α → ℕ → ℕ ⊕ α :=
  fun l n => List.foldl (fun s a => Sum.casesOn s (fun x => Nat.casesOn x (Sum.inr a) Sum.inl) Sum.inr) (Sum.inl n) l
hF : Primrec₂ F
this : Primrec fun p => Sum.casesOn (F p.fst p.snd) (fun x => none) some
n : ℕ
a : α
l : List α
IH :
  ∀ (n : ℕ),
    List.get? l n =
      Sum.rec (fun val => none) (fun val => some val)
        (List.foldl
          (fun s a => Sum.rec (fun val => Nat.rec (Sum.inr a) (fun n n_ih => Sum.inl n) val) (fun val => Sum.inr val) s)
          (Sum.inl n) l)
⊢ List.get? (a :: l) Nat.zero =
    Sum.rec (fun val => none) (fun val => some val)
      (List.foldl
        (fun s a => Sum.rec (fun val => Nat.rec (Sum.inr a) (fun n n_ih => Sum.inl n) val) (fun val => Sum.inr val) s)
        (Sum.inl Nat.zero) (a :: l))
dsimp
case cons.zero
α : Type u_1
β : Type ?u.254009
γ : Type ?u.254012
σ : Type ?u.254015
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
F : List α → ℕ → ℕ ⊕ α :=
  fun l n => List.foldl (fun s a => Sum.casesOn s (fun x => Nat.casesOn x (Sum.inr a) Sum.inl) Sum.inr) (Sum.inl n) l
hF : Primrec₂ F
this : Primrec fun p => Sum.casesOn (F p.fst p.snd) (fun x => none) some
n : ℕ
a : α
l : List α
⊢ some a =
    Sum.rec (fun val => none) (fun val => some val)
      (List.foldl
        (fun s a => Sum.rec (fun val => Nat.rec (Sum.inr a) (fun n n_ih => Sum.inl n) val) (fun val => Sum.inr val) s)
        (Sum.inr a) l)
case cons.zero
α : Type u_1
β : Type ?u.254009
γ : Type ?u.254012
σ : Type ?u.254015
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
F : List α → ℕ → ℕ ⊕ α :=
  fun l n => List.foldl (fun s a => Sum.casesOn s (fun x => Nat.casesOn x (Sum.inr a) Sum.inl) Sum.inr) (Sum.inl n) l
hF : Primrec₂ F
this : Primrec fun p => Sum.casesOn (F p.fst p.snd) (fun x => none) some
n : ℕ
a : α
l : List α
IH :
  ∀ (n : ℕ),
    List.get? l n =
      Sum.rec (fun val => none) (fun val => some val)
        (List.foldl
          (fun s a => Sum.rec (fun val => Nat.rec (Sum.inr a) (fun n n_ih => Sum.inl n) val) (fun val => Sum.inr val) s)
          (Sum.inl n) l)
⊢ some a =
    Sum.rec (fun val => none) (fun val => some val)
      (List.foldl
        (fun s a => Sum.rec (fun val => Nat.rec (Sum.inr a) (fun n n_ih => Sum.inl n) val) (fun val => Sum.inr val) s)
        (Sum.inr a) l)
clear IH
no goals
case cons.zero
α : Type u_1
β : Type ?u.254009
γ : Type ?u.254012
σ : Type ?u.254015
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
F : List α → ℕ → ℕ ⊕ α :=
  fun l n => List.foldl (fun s a => Sum.casesOn s (fun x => Nat.casesOn x (Sum.inr a) Sum.inl) Sum.inr) (Sum.inl n) l
hF : Primrec₂ F
this : Primrec fun p => Sum.casesOn (F p.fst p.snd) (fun x => none) some
n : ℕ
a : α
l : List α
⊢ some a =
    Sum.rec (fun val => none) (fun val => some val)
      (List.foldl
        (fun s a => Sum.rec (fun val => Nat.rec (Sum.inr a) (fun n n_ih => Sum.inl n) val) (fun val => Sum.inr val) s)
        (Sum.inr a) l)
induction' l with _ l IH <;> simp [*]
no goals
case cons.succ
α : Type u_1
β : Type ?u.254009
γ : Type ?u.254012
σ : Type ?u.254015
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
F : List α → ℕ → ℕ ⊕ α :=
  fun l n => List.foldl (fun s a => Sum.casesOn s (fun x => Nat.casesOn x (Sum.inr a) Sum.inl) Sum.inr) (Sum.inl n) l
hF : Primrec₂ F
this : Primrec fun p => Sum.casesOn (F p.fst p.snd) (fun x => none) some
n✝ : ℕ
a : α
l : List α
IH :
  ∀ (n : ℕ),
    List.get? l n =
      Sum.rec (fun val => none) (fun val => some val)
        (List.foldl
          (fun s a => Sum.rec (fun val => Nat.rec (Sum.inr a) (fun n n_ih => Sum.inl n) val) (fun val => Sum.inr val) s)
          (Sum.inl n) l)
n : ℕ
⊢ List.get? (a :: l) (Nat.succ n) =
    Sum.rec (fun val => none) (fun val => some val)
      (List.foldl
        (fun s a => Sum.rec (fun val => Nat.rec (Sum.inr a) (fun n n_ih => Sum.inl n) val) (fun val => Sum.inr val) s)
        (Sum.inl (Nat.succ n)) (a :: l))
apply IH