have lt₁ : e.unpair.1.pred.unpair.2 < e.unpair.1 :=
  lt_of_le_of_lt (Nat.unpair_right_le _) (Nat.pred_lt (fun eq => by simp[eq] at has))
α : Type u_1
α₁ : Type u_2
α₂ : Type u_3
β : Type u_4
γ : Type u_5
σ : Type u_6
τ : Type u_7
inst✝⁶ : Primcodable α
inst✝⁵ : Primcodable α₁
inst✝⁴ : Primcodable α₂
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable σ
inst✝ : Primcodable τ
f : σ → α × β → γ
hf : Primrec₂ f
h : Primrec₂ fun x p => some (Primrec.decodeZipWithRec f x p)
F : σ → ℕ → Option (List γ) := fun x n => (decode n).bind fun p => some (List.zipWith (fun a b => f x (a, b)) p.1 p.2)
x : σ
e : ℕ
a : α
as : List α
has : decode e.unpair.1 = some (a :: as)
b : β
bs : List β
hbs : decode e.unpair.2 = some (b :: bs)
⊢ e.unpair.1.pred.unpair.2.pair e.unpair.2.pred.unpair.2 < e
α : Type u_1
α₁ : Type u_2
α₂ : Type u_3
β : Type u_4
γ : Type u_5
σ : Type u_6
τ : Type u_7
inst✝⁶ : Primcodable α
inst✝⁵ : Primcodable α₁
inst✝⁴ : Primcodable α₂
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable σ
inst✝ : Primcodable τ
f : σ → α × β → γ
hf : Primrec₂ f
h : Primrec₂ fun x p => some (Primrec.decodeZipWithRec f x p)
F : σ → ℕ → Option (List γ) := fun x n => (decode n).bind fun p => some (List.zipWith (fun a b => f x (a, b)) p.1 p.2)
x : σ
e : ℕ
a : α
as : List α
has : decode e.unpair.1 = some (a :: as)
b : β
bs : List β
hbs : decode e.unpair.2 = some (b :: bs)
lt₁ : e.unpair.1.pred.unpair.2 < e.unpair.1
⊢ e.unpair.1.pred.unpair.2.pair e.unpair.2.pred.unpair.2 < e