Goal:
    A : Type  P : nat → A → Type  Q : A → Type  k : nat  l : list A
  ============================
   (Alli P k l → All Q l → Alli (λ (k : nat) (x : A), P k x × Q x) k l)


DEBUG:Going to execute:
induction 1

Goals:
    A : Type  P : nat → A → Type  Q : A → Type  n : nat
  ============================
   (All Q [] → Alli (λ (k : nat) (x : A), P k x × Q x) n [])

  
  A : Type
  P : nat → A → Type
  Q : A → Type
  n : nat
  hd : A
  tl : list A
  p : P n hd
  X : Alli P (S n) tl
  IHX : All Q tl → Alli (λ (k : nat) (x : A), P k x × Q x) (S n) tl
  ============================
   (All Q (hd :: tl) → Alli (λ (k : nat) (x : A), P k x × Q x) n (hd :: tl))


DEBUG:Going to execute:
constructor

Goals:
    A : Type  P : nat → A → Type  Q : A → Type  n : nat
  ============================
   (All Q [] → Alli (λ (k : nat) (x : A), P k x × Q x) n [])

  
  A : Type
  P : nat → A → Type
  Q : A → Type
  n : nat
  hd : A
  tl : list A
  p : P n hd
  X : Alli P (S n) tl
  IHX : All Q tl → Alli (λ (k : nat) (x : A), P k x × Q x) (S n) tl
  ============================
   (All Q (hd :: tl) → Alli (λ (k : nat) (x : A), P k x × Q x) n (hd :: tl))


DEBUG:Going to execute:
<coq-core.plugins.ltac::constructor@0>

Goals:
  
  A : Type
  P : nat → A → Type
  Q : A → Type
  n : nat
  hd : A
  tl : list A
  p : P n hd
  X : Alli P (S n) tl
  IHX : All Q tl → Alli (λ (k : nat) (x : A), P k x × Q x) (S n) tl
  X0 : All Q (hd :: tl)
  ============================
   (P n hd × Q hd)

  
  A : Type
  P : nat → A → Type
  Q : A → Type
  n : nat
  hd : A
  tl : list A
  p : P n hd
  X : Alli P (S n) tl
  IHX : All Q tl → Alli (λ (k : nat) (x : A), P k x × Q x) (S n) tl
  X0 : All Q (hd :: tl)
  ============================
   (Alli (λ (k : nat) (x : A), P k x × Q x) (S n) tl)


DEBUG:Going to execute:
try inversion X0