α : Type u_2
β : Type u_1
γ : Type ?u.316436
σ : Type ?u.316439
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f : α → List β
p : α → β → Bool
hf : Primrec f
hp : Primrec₂ p
a : α
⊢ List.foldr (fun b s => bif p a b then 0 else Nat.succ s) 0 (f a) = List.findIdx (p a) (f a)
α : Type u_2
β : Type u_1
γ : Type ?u.316436
σ : Type ?u.316439
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f : α → List β
p : α → β → Bool
hf : Primrec f
hp : Primrec₂ p
a : α
⊢ List.foldr (fun b s => bif p (a, b, s).fst (a, b, s).snd.fst then 0 else Nat.succ (a, b, s).snd.snd) 0 (f a) =
    List.findIdx (p a) (f a)
dsimp
no goals
α : Type u_2
β : Type u_1
γ : Type ?u.316436
σ : Type ?u.316439
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f : α → List β
p : α → β → Bool
hf : Primrec f
hp : Primrec₂ p
a : α
⊢ List.foldr (fun b s => bif p a b then 0 else Nat.succ s) 0 (f a) = List.findIdx (p a) (f a)
induction f a <;> simp [List.findIdx_cons, *]