Goal:
  
  A : Type
  x : A
  xs : list A
  f : A → bool
  H0 : ∀ f0 : A → bool,
         let l := xs in
         let g := λ (x : A) (_ : In x xs), f x in
         g = (λ (x : A) (_ : In x l), f0 x) → forallb_InP l g = forallb f0 l
  ============================
   (let H := CoreTactics.block in
    forallb_InP (x :: xs) (λ (x0 : A) (_ : In x0 (x :: xs)), f x0) =
    forallb f (x :: xs))


DEBUG:Going to execute:
cbn[eq_rect_r eq_rect] in hyp