Goal:
  
  A : Type
  P : nat → A → Type
  n : nat
  x : A
  Γ : list A
  IHΓ : All_fold (λ (Γ : list A) (d : A), P (n + #|Γ|) d) (List.rev Γ)
        → Alli P n Γ
  a1 : list A
  a : All_fold (λ (Γ : list A) (d : A), P (n + #|Γ|) d) a1
  ============================
   (x :: List.rev Γ = a1
    → let H := CoreTactics.block in
      let H0 := CoreTactics.block in Alli P n (Γ ++ [x]))


DEBUG:Going to execute:
destruct p || (case p; clear p)
Level 4: evaluation of term
raised the exception
Backtrace:


Could not find an instance for "DepElim.DependentEliminationPackage
                                  (All_fold
                                     (λ (Γ : list A) (d : A), P (n + #|Γ|) d)
                                     a1)"
in
environment:
A : Type
P : nat → A → Type
n : nat
x : A
Γ : list A
IHΓ : All_fold (λ (Γ : list A) (d : A), P (n + #|Γ|) d) (List.rev Γ)
      → Alli P n Γ
a1 : list A
a : All_fold (λ (Γ : list A) (d : A), P (n + #|Γ|) d) a1


Level 3: Backtrace:


Could not find an instance for "DepElim.DependentEliminationPackage
                                  (All_fold
                                     (λ (Γ : list A) (d : A), P (n + #|Γ|) d)
                                     a1)"
in
environment:
A : Type
P : nat → A → Type
n : nat
x : A
Γ : list A
IHΓ : All_fold (λ (Γ : list A) (d : A), P (n + #|Γ|) d) (List.rev Γ)
      → Alli P n Γ
a1 : list A
a : All_fold (λ (Γ : list A) (d : A), P (n + #|Γ|) d) a1

Level 2: Backtrace:


Could not find an instance for "DepElim.DependentEliminationPackage
                                  (All_fold
                                     (λ (Γ : list A) (d : A), P (n + #|Γ|) d)
                                     a1)"
in
environment:
A : Type
P : nat → A → Type
n : nat
x : A
Γ : list A
IHΓ : All_fold (λ (Γ : list A) (d : A), P (n + #|Γ|) d) (List.rev Γ)
      → Alli P n Γ
a1 : list A
a : All_fold (λ (Γ : list A) (d : A), P (n + #|Γ|) d) a1

Level 2: evaluation
raised the exception
Backtrace:


Could not find an instance for "DepElim.DependentEliminationPackage
                                  (All_fold
                                     (λ (Γ : list A) (d : A), P (n + #|Γ|) d)
                                     a1)"
in
environment:
A : Type
P : nat → A → Type
n : nat
x : A
Γ : list A
IHΓ : All_fold (λ (Γ : list A) (d : A), P (n + #|Γ|) d) (List.rev Γ)
      → Alli P n Γ
a1 : list A
a : All_fold (λ (Γ : list A) (d : A), P (n + #|Γ|) d) a1


Level 2: Backtrace:


Could not find an instance for "DepElim.DependentEliminationPackage
                                  (All_fold
                                     (λ (Γ : list A) (d : A), P (n + #|Γ|) d)
                                     a1)"
in
environment:
A : Type
P : nat → A → Type
n : nat
x : A
Γ : list A
IHΓ : All_fold (λ (Γ : list A) (d : A), P (n + #|Γ|) d) (List.rev Γ)
      → Alli P n Γ
a1 : list A
a : All_fold (λ (Γ : list A) (d : A), P (n + #|Γ|) d) a1

Level 2: Backtrace:


Could not find an instance for "DepElim.DependentEliminationPackage
                                  (All_fold
                                     (λ (Γ : list A) (d : A), P (n + #|Γ|) d)
                                     a1)"
in
environment:
A : Type
P : nat → A → Type
n : nat
x : A
Γ : list A
IHΓ : All_fold (λ (Γ : list A) (d : A), P (n + #|Γ|) d) (List.rev Γ)
      → Alli P n Γ
a1 : list A
a : All_fold (λ (Γ : list A) (d : A), P (n + #|Γ|) d) a1

Level 1: Backtrace:


Could not find an instance for "DepElim.DependentEliminationPackage
                                  (All_fold
                                     (λ (Γ : list A) (d : A), P (n + #|Γ|) d)
                                     a1)"
in
environment:
A : Type
P : nat → A → Type
n : nat
x : A
Γ : list A
IHΓ : All_fold (λ (Γ : list A) (d : A), P (n + #|Γ|) d) (List.rev Γ)
      → Alli P n Γ
a1 : list A
a : All_fold (λ (Γ : list A) (d : A), P (n + #|Γ|) d) a1

Level 1: evaluation
raised the exception
Backtrace:


Could not find an instance for "DepElim.DependentEliminationPackage
                                  (All_fold
                                     (λ (Γ : list A) (d : A), P (n + #|Γ|) d)
                                     a1)"
in
environment:
A : Type
P : nat → A → Type
n : nat
x : A
Γ : list A
IHΓ : All_fold (λ (Γ : list A) (d : A), P (n + #|Γ|) d) (List.rev Γ)
      → Alli P n Γ
a1 : list A
a : All_fold (λ (Γ : list A) (d : A), P (n + #|Γ|) d) a1


Level 1: Backtrace:


Could not find an instance for "DepElim.DependentEliminationPackage
                                  (All_fold
                                     (λ (Γ : list A) (d : A), P (n + #|Γ|) d)
                                     a1)"
in
environment:
A : Type
P : nat → A → Type
n : nat
x : A
Γ : list A
IHΓ : All_fold (λ (Γ : list A) (d : A), P (n + #|Γ|) d) (List.rev Γ)
      → Alli P n Γ
a1 : list A
a : All_fold (λ (Γ : list A) (d : A), P (n + #|Γ|) d) a1

Level 0: Backtrace:


Could not find an instance for "DepElim.DependentEliminationPackage
                                  (All_fold
                                     (λ (Γ : list A) (d : A), P (n + #|Γ|) d)
                                     a1)"
in
environment:
A : Type
P : nat → A → Type
n : nat
x : A
Γ : list A
IHΓ : All_fold (λ (Γ : list A) (d : A), P (n + #|Γ|) d) (List.rev Γ)
      → Alli P n Γ
a1 : list A
a : All_fold (λ (Γ : list A) (d : A), P (n + #|Γ|) d) a1