Goal:
  
  A : Type
  B : Type
  C : Type
  Q : C → Type
  P : C → A → Prop
  fn : ∀ x : A, (∀ y : C, Q y → P y x) → B
  x : A
  xs : list A
  h : ∀ y : C, Q y → ∥ All (P y) (x :: xs) ∥
  H : #|map_All fn xs (map_All_obligation_2 x xs h)| = #|xs|
  ============================
   (#|map_All fn (x :: xs) h| = #|x :: xs|)


DEBUG:Going to execute:
match goal with
           | hyp:context [ CoreTactics.block ]
             |- _ =>
                 cbn beta in hyp; eqns_specialize_eqs_block hyp;
                  cbn[eq_rect_r eq_rect] in hyp
           end
Level 1: Backtrace:

No matching clauses for match.

Goals:
  
  A : Type
  B : Type
  C : Type
  Q : C → Type
  P : C → A → Prop
  fn : ∀ x : A, (∀ y : C, Q y → P y x) → B
  Hl : ∀ y : C, Q y → ∥ All (P y) [] ∥
  ============================
   (#|map_All fn [] Hl| = #|[]|)

  
  A : Type
  B : Type
  C : Type
  Q : C → Type
  P : C → A → Prop
  fn : ∀ x : A, (∀ y : C, Q y → P y x) → B
  x : A
  xs : list A
  h : ∀ y : C, Q y → ∥ All (P y) (x :: xs) ∥
  H : #|map_All fn xs (map_All_obligation_2 x xs h)| = #|xs|
  ============================
   (#|map_All fn (x :: xs) h| = #|x :: xs|)


DEBUG:Going to execute:
tac c
Level 1: Backtrace:

No matching clauses for match.

Goals:
  
  A : Type
  B : Type
  C : Type
  Q : C → Type
  P : C → A → Prop
  fn : ∀ x : A, (∀ y : C, Q y → P y x) → B
  Hl : ∀ y : C, Q y → ∥ All (P y) [] ∥
  ============================
   (#|map_All fn [] Hl| = #|[]|)

  
  A : Type
  B : Type
  C : Type
  Q : C → Type
  P : C → A → Prop
  fn : ∀ x : A, (∀ y : C, Q y → P y x) → B
  x : A
  xs : list A
  h : ∀ y : C, Q y → ∥ All (P y) (x :: xs) ∥
  H : #|map_All fn xs (map_All_obligation_2 x xs h)| = #|xs|
  ============================
   (#|map_All fn (x :: xs) h| = #|x :: xs|)


DEBUG:Going to execute:
idtac

Goals:
  
  A : Type
  B : Type
  C : Type
  Q : C → Type
  P : C → A → Prop
  fn : ∀ x : A, (∀ y : C, Q y → P y x) → B
  Hl : ∀ y : C, Q y → ∥ All (P y) [] ∥
  ============================
   (#|map_All fn [] Hl| = #|[]|)

  
  A : Type
  B : Type
  C : Type
  Q : C → Type
  P : C → A → Prop
  fn : ∀ x : A, (∀ y : C, Q y → P y x) → B
  x : A
  xs : list A
  h : ∀ y : C, Q y → ∥ All (P y) (x :: xs) ∥
  H : #|map_All fn xs (map_All_obligation_2 x xs h)| = #|xs|
  ============================
   (#|map_All fn (x :: xs) h| = #|x :: xs|)


DEBUG:Going to execute:
cbn
Level 2: evaluation returns
idtac
where
c := map_All fn l Hl
of type
constr of type tacvalue

Level 2: evaluation returns
idtac
where
c := map_All fn l Hl
of type
constr of type tacvalue


Goals:
  
  A : Type
  B : Type
  C : Type
  Q : C → Type
  P : C → A → Prop
  fn : ∀ x : A, (∀ y : C, Q y → P y x) → B
  Hl : ∀ y : C, Q y → ∥ All (P y) [] ∥
  ============================
   (0 = 0)

  
  A : Type
  B : Type
  C : Type
  Q : C → Type
  P : C → A → Prop
  fn : ∀ x : A, (∀ y : C, Q y → P y x) → B
  x : A
  xs : list A
  h : ∀ y : C, Q y → ∥ All (P y) (x :: xs) ∥
  H : #|map_All fn xs (map_All_obligation_2 x xs h)| = #|xs|
  ============================
   (S #|map_All fn xs (map_All_obligation_2 x xs h)| = S #|xs|)


DEBUG:Going to execute:
congruence

Goals:
  
  A : Type
  B : Type
  C : Type
  Q : C → Type
  P : C → A → Prop
  fn : ∀ x : A, (∀ y : C, Q y → P y x) → B
  Hl : ∀ y : C, Q y → ∥ All (P y) [] ∥
  ============================
   (0 = 0)

  
  A : Type
  B : Type
  C : Type
  Q : C → Type
  P : C → A → Prop
  fn : ∀ x : A, (∀ y : C, Q y → P y x) → B
  x : A
  xs : list A
  h : ∀ y : C, Q y → ∥ All (P y) (x :: xs) ∥
  H : #|map_All fn xs (map_All_obligation_2 x xs h)| = #|xs|
  ============================
   (S #|map_All fn xs (map_All_obligation_2 x xs h)| = S #|xs|)


DEBUG:Going to execute:
<coq-core.plugins.cc::cc@0> $1