α : Type u_3
β : Type u_1
γ : Type ?u.250840
σ : Type u_2
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f : α → List β
g : α → σ
h : α → β × List β × σ → σ
hf : Primrec f
hg : Primrec g
hh : Primrec₂ h
F : α → List β × σ := fun a => List.foldr (fun b s => (b :: s.fst, h a (b, s))) ([], g a) (f a)
this : Primrec F
a : α
⊢ F a = (f a, List.recOn (f a) (g a) fun b l IH => h a (b, l, IH))
α : Type u_3
β : Type u_1
γ : Type ?u.250840
σ : Type u_2
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f : α → List β
g : α → σ
h : α → β × List β × σ → σ
hf : Primrec f
hg : Primrec g
hh : Primrec₂ h
F : α → List β × σ := fun a => List.foldr (fun b s => (b :: s.fst, h a (b, s))) ([], g a) (f a)
this : Primrec F
a : α
⊢ (F a).snd = List.recOn (f a) (g a) fun b l IH => h a (b, l, IH)
suffices F a = (f a, List.recOn (f a) (g a) fun b l IH => h a (b, l, IH)) by rw [this]
α : Type u_3
β : Type u_1
γ : Type ?u.250840
σ : Type u_2
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f : α → List β
g : α → σ
h : α → β × List β × σ → σ
hf : Primrec f
hg : Primrec g
hh : Primrec₂ h
F : α → List β × σ := fun a => List.foldr (fun b s => (b :: s.fst, h a (b, s))) ([], g a) (f a)
this : Primrec F
a : α
⊢ List.foldr (fun b s => (b :: s.fst, h a (b, s))) ([], g a) (f a) =
    (f a, List.rec (g a) (fun b l IH => h a (b, l, IH)) (f a))
α : Type u_3
β : Type u_1
γ : Type ?u.250840
σ : Type u_2
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f : α → List β
g : α → σ
h : α → β × List β × σ → σ
hf : Primrec f
hg : Primrec g
hh : Primrec₂ h
F : α → List β × σ := fun a => List.foldr (fun b s => (b :: s.fst, h a (b, s))) ([], g a) (f a)
this : Primrec F
a : α
⊢ F a = (f a, List.recOn (f a) (g a) fun b l IH => h a (b, l, IH))
dsimp
no goals
α : Type u_3
β : Type u_1
γ : Type ?u.250840
σ : Type u_2
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f : α → List β
g : α → σ
h : α → β × List β × σ → σ
hf : Primrec f
hg : Primrec g
hh : Primrec₂ h
F : α → List β × σ := fun a => List.foldr (fun b s => (b :: s.fst, h a (b, s))) ([], g a) (f a)
this : Primrec F
a : α
⊢ List.foldr (fun b s => (b :: s.fst, h a (b, s))) ([], g a) (f a) =
    (f a, List.rec (g a) (fun b l IH => h a (b, l, IH)) (f a))
induction' f a with b l IH <;> simp [*]
no goals
α : Type u_3
β : Type u_1
γ : Type ?u.250840
σ : Type u_2
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f : α → List β
g : α → σ
h : α → β × List β × σ → σ
hf : Primrec f
hg : Primrec g
hh : Primrec₂ h
F : α → List β × σ := fun a => List.foldr (fun b s => (b :: s.fst, h a (b, s))) ([], g a) (f a)
this✝ : Primrec F
a : α
this : F a = (f a, List.recOn (f a) (g a) fun b l IH => h a (b, l, IH))
⊢ (F a).snd = List.recOn (f a) (g a) fun b l IH => h a (b, l, IH)
rw [this]