Goal:
    A : Type
  ============================
   (∀ (l : list A) (l0 : ∀ x : A, In x l → bool) (H := CoreTactics.block) 
      (f : A → bool) (l1 : list A) (g : ∀ x : A, In x l1 → bool),
      g = (λ (x : A) (_ : In x l1), f x)
      → {| pr1 := l; pr2 := l0 |} = {| pr1 := l1; pr2 := g |}
        → forallb_InP l l0 = forallb_InP l1 g
          → let H0 := CoreTactics.block in forallb_InP l1 g = forallb f l1)


DEBUG:Going to execute:
make_refine n ltac:(uconstr:((c _)))
DEBUG LTAC Evaluated term: 2
Level 5: constr:(n)
 has value 
2