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:
<coq-equations.plugin::refine_ho@0> $1
DEBUG LTAC Evaluated term: (fun_elim ?P ?f ?f0)

Goals:
  
  ============================
   (∀ (A B : Type) (f : ∀ x : A, In x [] → B),
      (λ (A0 B0 : Type) (l : list A0) (f0 : ∀ x : A0, In x l → B0) 
         (x : list B0),
         ∀ (H := CoreTactics.block) (A1 B1 : Type) 
           (f1 : A1 → B1) (l0 : list A1) (g : ∀ x0 : A1, In x0 l0 → B1),
           g = (λ (x0 : A1) (_ : In x0 l0), f1 x0)
           → ∀ eqargs : {|
                          pr1 := A0;
                          pr2 :=
                            {| pr1 := B0; pr2 := {| pr1 := l; pr2 := f0 |} |}
                        |} =
                        {|
                          pr1 := A1;
                          pr2 :=
                            {| pr1 := B1; pr2 := {| pr1 := l0; pr2 := g |} |}
                        |},
               eq_rect
                 {|
                   pr1 := A0;
                   pr2 := {| pr1 := B0; pr2 := {| pr1 := l; pr2 := f0 |} |}
                 |}
                 (λ projs : sigma
                              (λ A2 : Type,
                                 sigma
                                   (λ B2 : Type,
                                      sigma
                                        (λ l1 : list A2,
                                           ∀ x0 : A2, In x0 l1 → B2))),
                    list (pr1 (pr2 projs))) x
                 {|
                   pr1 := A1;
                   pr2 := {| pr1 := B1; pr2 := {| pr1 := l0; pr2 := g |} |}
                 |} eqargs = map_In l0 g
               → let H0 := CoreTactics.block in map_In l0 g = map f1 l0) A B
        [] f [])

  
  ============================
   (∀ (A B : Type) (x : A) (xs : list A) (f : ∀ x0 : A, In x0 (x :: xs) → B),
      (λ (A0 B0 : Type) (l : list A0) (f0 : ∀ x0 : A0, In x0 l → B0) 
         (x0 : list B0),
         ∀ (H := CoreTactics.block) (A1 B1 : Type) 
           (f1 : A1 → B1) (l0 : list A1) (g : ∀ x1 : A1, In x1 l0 → B1),
           g = (λ (x1 : A1) (_ : In x1 l0), f1 x1)
           → ∀ eqargs : {|
                          pr1 := A0;
                          pr2 :=
                            {| pr1 := B0; pr2 := {| pr1 := l; pr2 := f0 |} |}
                        |} =
                        {|
                          pr1 := A1;
                          pr2 :=
                            {| pr1 := B1; pr2 := {| pr1 := l0; pr2 := g |} |}
                        |},
               eq_rect
                 {|
                   pr1 := A0;
                   pr2 := {| pr1 := B0; pr2 := {| pr1 := l; pr2 := f0 |} |}
                 |}
                 (λ projs : sigma
                              (λ A2 : Type,
                                 sigma
                                   (λ B2 : Type,
                                      sigma
                                        (λ l1 : list A2,
                                           ∀ x1 : A2, In x1 l1 → B2))),
                    list (pr1 (pr2 projs))) x0
                 {|
                   pr1 := A1;
                   pr2 := {| pr1 := B1; pr2 := {| pr1 := l0; pr2 := g |} |}
                 |} eqargs = map_In l0 g
               → let H0 := CoreTactics.block in map_In l0 g = map f1 l0) A B
        xs
        (λ (x0 : A) (H : In x0 xs),
           f x0 (map_In_obligations_obligation_2 A x xs x0 H))
        (map_In xs
           (λ (x0 : A) (H : In x0 xs),
              f x0 (map_In_obligations_obligation_2 A x xs x0 H)))
      → (λ (A0 B0 : Type) (l : list A0) (f0 : ∀ x0 : A0, In x0 l → B0) 
           (x0 : list B0),
           ∀ (H := CoreTactics.block) (A1 B1 : Type) 
             (f1 : A1 → B1) (l0 : list A1) (g : ∀ x1 : A1, In x1 l0 → B1),
             g = (λ (x1 : A1) (_ : In x1 l0), f1 x1)
             → ∀ eqargs : {|
                            pr1 := A0;
                            pr2 :=
                              {|
                                pr1 := B0; pr2 := {| pr1 := l; pr2 := f0 |}
                              |}
                          |} =
                          {|
                            pr1 := A1;
                            pr2 :=
                              {|
                                pr1 := B1; pr2 := {| pr1 := l0; pr2 := g |}
                              |}
                          |},
                 eq_rect
                   {|
                     pr1 := A0;
                     pr2 := {| pr1 := B0; pr2 := {| pr1 := l; pr2 := f0 |} |}
                   |}
                   (λ projs : sigma
                                (λ A2 : Type,
                                   sigma
                                     (λ B2 : Type,
                                        sigma
                                          (λ l1 : list A2,
                                             ∀ x1 : A2, In x1 l1 → B2))),
                      list (pr1 (pr2 projs))) x0
                   {|
                     pr1 := A1;
                     pr2 := {| pr1 := B1; pr2 := {| pr1 := l0; pr2 := g |} |}
                   |} eqargs = map_In l0 g
                 → let H0 := CoreTactics.block in map_In l0 g = map f1 l0) A
          B (x :: xs) f
          (f x (map_In_obligations_obligation_1 A x xs)
           :: map_In xs
                (λ (x0 : A) (H : In x0 xs),
                   f x0 (map_In_obligations_obligation_2 A x xs x0 H))))


DEBUG:Going to execute:
intros

Goals:
    A : Type  B : Type  f : ∀ x : A, In x [] → B
  ============================
   ((λ (A B : Type) (l : list A) (f : ∀ x : A, In x l → B) (x : list B),
       ∀ (H := CoreTactics.block) (A0 B0 : Type) (f0 : A0 → B0) 
         (l0 : list A0) (g : ∀ x0 : A0, In x0 l0 → B0),
         g = (λ (x0 : A0) (_ : In x0 l0), f0 x0)
         → ∀ eqargs : {|
                        pr1 := A;
                        pr2 :=
                          {| pr1 := B; pr2 := {| pr1 := l; pr2 := f |} |}
                      |} =
                      {|
                        pr1 := A0;
                        pr2 :=
                          {| pr1 := B0; pr2 := {| pr1 := l0; pr2 := g |} |}
                      |},
             eq_rect
               {|
                 pr1 := A;
                 pr2 := {| pr1 := B; pr2 := {| pr1 := l; pr2 := f |} |}
               |}
               (λ projs : sigma
                            (λ A1 : Type,
                               sigma
                                 (λ B1 : Type,
                                    sigma
                                      (λ l1 : list A1,
                                         ∀ x0 : A1, In x0 l1 → B1))),
                  list (pr1 (pr2 projs))) x
               {|
                 pr1 := A0;
                 pr2 := {| pr1 := B0; pr2 := {| pr1 := l0; pr2 := g |} |}
               |} eqargs = map_In l0 g
             → let H0 := CoreTactics.block in map_In l0 g = map f0 l0) A B []
      f [])

  
  A : Type
  B : Type
  x : A
  xs : list A
  f : ∀ x0 : A, In x0 (x :: xs) → B
  H : (λ (A B : Type) (l : list A) (f : ∀ x : A, In x l → B) (x : list B),
         ∀ (H := CoreTactics.block) (A0 B0 : Type) 
           (f0 : A0 → B0) (l0 : list A0) (g : ∀ x0 : A0, In x0 l0 → B0),
           g = (λ (x0 : A0) (_ : In x0 l0), f0 x0)
           → ∀ eqargs : {|
                          pr1 := A;
                          pr2 :=
                            {| pr1 := B; pr2 := {| pr1 := l; pr2 := f |} |}
                        |} =
                        {|
                          pr1 := A0;
                          pr2 :=
                            {| pr1 := B0; pr2 := {| pr1 := l0; pr2 := g |} |}
                        |},
               eq_rect
                 {|
                   pr1 := A;
                   pr2 := {| pr1 := B; pr2 := {| pr1 := l; pr2 := f |} |}
                 |}
                 (λ projs : sigma
                              (λ A1 : Type,
                                 sigma
                                   (λ B1 : Type,
                                      sigma
                                        (λ l1 : list A1,
                                           ∀ x0 : A1, In x0 l1 → B1))),
                    list (pr1 (pr2 projs))) x
                 {|
                   pr1 := A0;
                   pr2 := {| pr1 := B0; pr2 := {| pr1 := l0; pr2 := g |} |}
                 |} eqargs = map_In l0 g
               → let H0 := CoreTactics.block in map_In l0 g = map f0 l0) A B
        xs
        (λ (x0 : A) (H : In x0 xs),
           f x0 (map_In_obligations_obligation_2 A x xs x0 H))
        (map_In xs
           (λ (x0 : A) (H : In x0 xs),
              f x0 (map_In_obligations_obligation_2 A x xs x0 H)))
  ============================
   ((λ (A B : Type) (l : list A) (f : ∀ x : A, In x l → B) (x : list B),
       ∀ (H := CoreTactics.block) (A0 B0 : Type) (f0 : A0 → B0) 
         (l0 : list A0) (g : ∀ x0 : A0, In x0 l0 → B0),
         g = (λ (x0 : A0) (_ : In x0 l0), f0 x0)
         → ∀ eqargs : {|
                        pr1 := A;
                        pr2 :=
                          {| pr1 := B; pr2 := {| pr1 := l; pr2 := f |} |}
                      |} =
                      {|
                        pr1 := A0;
                        pr2 :=
                          {| pr1 := B0; pr2 := {| pr1 := l0; pr2 := g |} |}
                      |},
             eq_rect
               {|
                 pr1 := A;
                 pr2 := {| pr1 := B; pr2 := {| pr1 := l; pr2 := f |} |}
               |}
               (λ projs : sigma
                            (λ A1 : Type,
                               sigma
                                 (λ B1 : Type,
                                    sigma
                                      (λ l1 : list A1,
                                         ∀ x0 : A1, In x0 l1 → B1))),
                  list (pr1 (pr2 projs))) x
               {|
                 pr1 := A0;
                 pr2 := {| pr1 := B0; pr2 := {| pr1 := l0; pr2 := g |} |}
               |} eqargs = map_In l0 g
             → let H0 := CoreTactics.block in map_In l0 g = map f0 l0) A B
      (x :: xs) f
      (f x (map_In_obligations_obligation_1 A x xs)
       :: map_In xs
            (λ (x0 : A) (H : In x0 xs),
               f x0 (map_In_obligations_obligation_2 A x xs x0 H))))


DEBUG:Going to execute:
cbv beta

Goals:
    A : Type  B : Type  f : ∀ x : A, In x [] → B
  ============================
   (∀ (H := CoreTactics.block) (A0 B0 : Type) (f0 : A0 → B0) 
      (l : list A0) (g : ∀ x : A0, In x l → B0),
      g = (λ (x : A0) (_ : In x l), f0 x)
      → ∀ eqargs : {|
                     pr1 := A;
                     pr2 := {| pr1 := B; pr2 := {| pr1 := []; pr2 := f |} |}
                   |} =
                   {|
                     pr1 := A0;
                     pr2 := {| pr1 := B0; pr2 := {| pr1 := l; pr2 := g |} |}
                   |},
          eq_rect
            {|
              pr1 := A;
              pr2 := {| pr1 := B; pr2 := {| pr1 := []; pr2 := f |} |}
            |}
            (λ projs : sigma
                         (λ A : Type,
                            sigma
                              (λ B : Type,
                                 sigma (λ l0 : list A, ∀ x : A, In x l0 → B))),
               list (pr1 (pr2 projs))) []
            {|
              pr1 := A0;
              pr2 := {| pr1 := B0; pr2 := {| pr1 := l; pr2 := g |} |}
            |} eqargs = map_In l g
          → let H0 := CoreTactics.block in map_In l g = map f0 l)

  
  A : Type
  B : Type
  x : A
  xs : list A
  f : ∀ x0 : A, In x0 (x :: xs) → B
  H : (λ (A B : Type) (l : list A) (f : ∀ x : A, In x l → B) (x : list B),
         ∀ (H := CoreTactics.block) (A0 B0 : Type) 
           (f0 : A0 → B0) (l0 : list A0) (g : ∀ x0 : A0, In x0 l0 → B0),
           g = (λ (x0 : A0) (_ : In x0 l0), f0 x0)
           → ∀ eqargs : {|
                          pr1 := A;
                          pr2 :=
                            {| pr1 := B; pr2 := {| pr1 := l; pr2 := f |} |}
                        |} =
                        {|
                          pr1 := A0;
                          pr2 :=
                            {| pr1 := B0; pr2 := {| pr1 := l0; pr2 := g |} |}
                        |},
               eq_rect
                 {|
                   pr1 := A;
                   pr2 := {| pr1 := B; pr2 := {| pr1 := l; pr2 := f |} |}
                 |}
                 (λ projs : sigma
                              (λ A1 : Type,
                                 sigma
                                   (λ B1 : Type,
                                      sigma
                                        (λ l1 : list A1,
                                           ∀ x0 : A1, In x0 l1 → B1))),
                    list (pr1 (pr2 projs))) x
                 {|
                   pr1 := A0;
                   pr2 := {| pr1 := B0; pr2 := {| pr1 := l0; pr2 := g |} |}
                 |} eqargs = map_In l0 g
               → let H0 := CoreTactics.block in map_In l0 g = map f0 l0) A B
        xs
        (λ (x0 : A) (H : In x0 xs),
           f x0 (map_In_obligations_obligation_2 A x xs x0 H))
        (map_In xs
           (λ (x0 : A) (H : In x0 xs),
              f x0 (map_In_obligations_obligation_2 A x xs x0 H)))
  ============================
   (∀ (H := CoreTactics.block) (A0 B0 : Type) (f0 : A0 → B0) 
      (l : list A0) (g : ∀ x : A0, In x l → B0),
      g = (λ (x : A0) (_ : In x l), f0 x)
      → ∀ eqargs : {|
                     pr1 := A;
                     pr2 :=
                       {| pr1 := B; pr2 := {| pr1 := x :: xs; pr2 := f |} |}
                   |} =
                   {|
                     pr1 := A0;
                     pr2 := {| pr1 := B0; pr2 := {| pr1 := l; pr2 := g |} |}
                   |},
          eq_rect
            {|
              pr1 := A;
              pr2 := {| pr1 := B; pr2 := {| pr1 := x :: xs; pr2 := f |} |}
            |}
            (λ projs : sigma
                         (λ A : Type,
                            sigma
                              (λ B : Type,
                                 sigma (λ l0 : list A, ∀ x : A, In x l0 → B))),
               list (pr1 (pr2 projs)))
            (f x (map_In_obligations_obligation_1 A x xs)
             :: map_In xs
                  (λ (x0 : A) (H0 : In x0 xs),
                     f x0 (map_In_obligations_obligation_2 A x xs x0 H0)))
            {|
              pr1 := A0;
              pr2 := {| pr1 := B0; pr2 := {| pr1 := l; pr2 := g |} |}
            |} eqargs = map_In l g
          → let H0 := CoreTactics.block in map_In l g = map f0 l)


DEBUG:Going to execute:
DepElim.simplify_dep_elim

Goals:
    A : Type  B : Type  f : ∀ x : A, In x [] → B
  ============================
   (∀ (H := CoreTactics.block) (A0 B0 : Type) (f0 : A0 → B0) 
      (l : list A0) (g : ∀ x : A0, In x l → B0),
      g = (λ (x : A0) (_ : In x l), f0 x)
      → ∀ eqargs : {|
                     pr1 := A;
                     pr2 := {| pr1 := B; pr2 := {| pr1 := []; pr2 := f |} |}
                   |} =
                   {|
                     pr1 := A0;
                     pr2 := {| pr1 := B0; pr2 := {| pr1 := l; pr2 := g |} |}
                   |},
          eq_rect
            {|
              pr1 := A;
              pr2 := {| pr1 := B; pr2 := {| pr1 := []; pr2 := f |} |}
            |}
            (λ projs : sigma
                         (λ A : Type,
                            sigma
                              (λ B : Type,
                                 sigma (λ l0 : list A, ∀ x : A, In x l0 → B))),
               list (pr1 (pr2 projs))) []
            {|
              pr1 := A0;
              pr2 := {| pr1 := B0; pr2 := {| pr1 := l; pr2 := g |} |}
            |} eqargs = map_In l g
          → let H0 := CoreTactics.block in map_In l g = map f0 l)

  
  A : Type
  B : Type
  x : A
  xs : list A
  f : ∀ x0 : A, In x0 (x :: xs) → B
  H : (λ (A B : Type) (l : list A) (f : ∀ x : A, In x l → B) (x : list B),
         ∀ (H := CoreTactics.block) (A0 B0 : Type) 
           (f0 : A0 → B0) (l0 : list A0) (g : ∀ x0 : A0, In x0 l0 → B0),
           g = (λ (x0 : A0) (_ : In x0 l0), f0 x0)
           → ∀ eqargs : {|
                          pr1 := A;
                          pr2 :=
                            {| pr1 := B; pr2 := {| pr1 := l; pr2 := f |} |}
                        |} =
                        {|
                          pr1 := A0;
                          pr2 :=
                            {| pr1 := B0; pr2 := {| pr1 := l0; pr2 := g |} |}
                        |},
               eq_rect
                 {|
                   pr1 := A;
                   pr2 := {| pr1 := B; pr2 := {| pr1 := l; pr2 := f |} |}
                 |}
                 (λ projs : sigma
                              (λ A1 : Type,
                                 sigma
                                   (λ B1 : Type,
                                      sigma
                                        (λ l1 : list A1,
                                           ∀ x0 : A1, In x0 l1 → B1))),
                    list (pr1 (pr2 projs))) x
                 {|
                   pr1 := A0;
                   pr2 := {| pr1 := B0; pr2 := {| pr1 := l0; pr2 := g |} |}
                 |} eqargs = map_In l0 g
               → let H0 := CoreTactics.block in map_In l0 g = map f0 l0) A B
        xs
        (λ (x0 : A) (H : In x0 xs),
           f x0 (map_In_obligations_obligation_2 A x xs x0 H))
        (map_In xs
           (λ (x0 : A) (H : In x0 xs),
              f x0 (map_In_obligations_obligation_2 A x xs x0 H)))
  ============================
   (∀ (H := CoreTactics.block) (A0 B0 : Type) (f0 : A0 → B0) 
      (l : list A0) (g : ∀ x : A0, In x l → B0),
      g = (λ (x : A0) (_ : In x l), f0 x)
      → ∀ eqargs : {|
                     pr1 := A;
                     pr2 :=
                       {| pr1 := B; pr2 := {| pr1 := x :: xs; pr2 := f |} |}
                   |} =
                   {|
                     pr1 := A0;
                     pr2 := {| pr1 := B0; pr2 := {| pr1 := l; pr2 := g |} |}
                   |},
          eq_rect
            {|
              pr1 := A;
              pr2 := {| pr1 := B; pr2 := {| pr1 := x :: xs; pr2 := f |} |}
            |}
            (λ projs : sigma
                         (λ A : Type,
                            sigma
                              (λ B : Type,
                                 sigma (λ l0 : list A, ∀ x : A, In x l0 → B))),
               list (pr1 (pr2 projs)))
            (f x (map_In_obligations_obligation_1 A x xs)
             :: map_In xs
                  (λ (x0 : A) (H0 : In x0 xs),
                     f x0 (map_In_obligations_obligation_2 A x xs x0 H0)))
            {|
              pr1 := A0;
              pr2 := {| pr1 := B0; pr2 := {| pr1 := l; pr2 := g |} |}
            |} eqargs = map_In l g
          → let H0 := CoreTactics.block in map_In l g = map f0 l)


DEBUG:Going to execute:
repeat DepElim.simplify_one_dep_elim