Goal:
    A : Type  B : Type
  ============================
   (∀ (l : list A) (l0 : ∀ x : A, In x l → B) (H := CoreTactics.block) 
      (f : A → B) (l1 : list A) (g : ∀ x : A, In x l1 → B),
      g = (λ (x : A) (_ : In x l1), f x)
      → {| pr1 := l; pr2 := l0 |} = {| pr1 := l1; pr2 := g |}
        → map_InP l l0 = map_InP l1 g
          → let H0 := CoreTactics.block in map_InP l1 g = map 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