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:
unshelve refine_ho elimt; intros; cbv beta