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:
let elimt := make_refine elimn elimc in
           unshelve refine_ho elimt; intros; cbv beta;
            DepElim.simplify_dep_elim; CoreTactics.intros_until_block;
            DepElim.simplify_dep_elim;
            cbn beta iota
             delta [Prop.Logic.transport Logic.eq_elim Logic.eq_elim_r
                   eq_rect DepElim.pack_sigma_eq
                   DepElim.pack_sigma_eq_nondep] in *;
            DepElim.simplify_IH_hyps; CoreTactics.unblock_goal;
            DepElim.simplify_IH_hyps; tac c