Goal:
  
  ============================
   (∀ (A B : Type) (l : list A) (l0 : ∀ x : A, In x l → B) 
      (H := CoreTactics.block) (A0 B0 : Type) (f : A0 → B0) 
      (l1 : list A0) (g : ∀ x : A0, In x l1 → B0),
      g = (λ (x : A0) (_ : In x l1), f x)
      → ∀ eqargs : {|
                     pr1 := A;
                     pr2 := {| pr1 := B; pr2 := {| pr1 := l; pr2 := l0 |} |}
                   |} =
                   {|
                     pr1 := A0;
                     pr2 := {| pr1 := B0; pr2 := {| pr1 := l1; pr2 := g |} |}
                   |},
          eq_rect
            {|
              pr1 := A;
              pr2 := {| pr1 := B; pr2 := {| pr1 := l; pr2 := l0 |} |}
            |}
            (λ projs : sigma
                         (λ A1 : Type,
                            sigma
                              (λ B1 : Type,
                                 sigma
                                   (λ l2 : list A1, ∀ x : A1, In x l2 → B1))),
               list (pr1 (pr2 projs))) (map_In l l0)
            {|
              pr1 := A0;
              pr2 := {| pr1 := B0; pr2 := {| pr1 := l1; pr2 := g |} |}
            |} eqargs = map_In l1 g
          → let H0 := CoreTactics.block in map_In 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