Goal:
    A : Type  P : nat → A → Type  Q : nat → A → Type  n : nat  l : list A
  ============================
   (Alli P n l → Alli Q n l → Alli (Trel_conj P Q) n l)


DEBUG:Going to execute:
induction 1

Goals:
    A : Type  P : nat → A → Type  Q : nat → A → Type  n : nat
  ============================
   (Alli Q n [] → Alli (Trel_conj P Q) n [])

  
  A : Type
  P : nat → A → Type
  Q : nat → A → Type
  n : nat
  hd : A
  tl : list A
  p : P n hd
  X : Alli P (S n) tl
  IHX : Alli Q (S n) tl → Alli (Trel_conj P Q) (S n) tl
  ============================
   (Alli Q n (hd :: tl) → Alli (Trel_conj P Q) n (hd :: tl))


DEBUG:Going to execute:
intros Hq

Goals:
  
  A : Type
  P : nat → A → Type
  Q : nat → A → Type
  n : nat
  Hq : Alli Q n []
  ============================
   (Alli (Trel_conj P Q) n [])

  
  A : Type
  P : nat → A → Type
  Q : nat → A → Type
  n : nat
  hd : A
  tl : list A
  p : P n hd
  X : Alli P (S n) tl
  IHX : Alli Q (S n) tl → Alli (Trel_conj P Q) (S n) tl
  Hq : Alli Q n (hd :: tl)
  ============================
   (Alli (Trel_conj P Q) n (hd :: tl))


DEBUG:Going to execute:
inv Hq

Goals:
  
  A : Type
  P : nat → A → Type
  Q : nat → A → Type
  n : nat
  Hq : Alli Q n []
  ============================
   (Alli (Trel_conj P Q) n [])

  
  A : Type
  P : nat → A → Type
  Q : nat → A → Type
  n : nat
  hd : A
  tl : list A
  p : P n hd
  X : Alli P (S n) tl
  IHX : Alli Q (S n) tl → Alli (Trel_conj P Q) (S n) tl
  Hq : Alli Q n (hd :: tl)
  ============================
   (Alli (Trel_conj P Q) n (hd :: tl))


DEBUG:Going to execute:
fun H => inversion_clear H

Goals:
  
  A : Type
  P : nat → A → Type
  Q : nat → A → Type
  n : nat
  Hq : Alli Q n []
  ============================
   (Alli (Trel_conj P Q) n [])

  
  A : Type
  P : nat → A → Type
  Q : nat → A → Type
  n : nat
  hd : A
  tl : list A
  p : P n hd
  X : Alli P (S n) tl
  IHX : Alli Q (S n) tl → Alli (Trel_conj P Q) (S n) tl
  Hq : Alli Q n (hd :: tl)
  ============================
   (Alli (Trel_conj P Q) n (hd :: tl))


DEBUG:Going to execute:
inversion_clear H

Goals:
    A : Type  P : nat → A → Type  Q : nat → A → Type  n : nat
  ============================
   (Alli (Trel_conj P Q) n [])

  
  A : Type
  P : nat → A → Type
  Q : nat → A → Type
  n : nat
  hd : A
  tl : list A
  p : P n hd
  X : Alli P (S n) tl
  IHX : Alli Q (S n) tl → Alli (Trel_conj P Q) (S n) tl
  X0 : Q n hd
  X1 : Alli Q (S n) tl
  ============================
   (Alli (Trel_conj P Q) n (hd :: tl))


DEBUG:Going to execute:
constructor
Level 1: evaluation returns
inversion_clear H
where
H := Hq
of type
ident of type tacvalue

Level 1: evaluation returns
inversion_clear H
where
H := Hq
of type
ident of type tacvalue


Goals:
    A : Type  P : nat → A → Type  Q : nat → A → Type  n : nat
  ============================
   (Alli (Trel_conj P Q) n [])

  
  A : Type
  P : nat → A → Type
  Q : nat → A → Type
  n : nat
  hd : A
  tl : list A
  p : P n hd
  X : Alli P (S n) tl
  IHX : Alli Q (S n) tl → Alli (Trel_conj P Q) (S n) tl
  X0 : Q n hd
  X1 : Alli Q (S n) tl
  ============================
   (Alli (Trel_conj P Q) n (hd :: tl))


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

Goals:
  
  A : Type
  P : nat → A → Type
  Q : nat → A → Type
  n : nat
  hd : A
  tl : list A
  p : P n hd
  X : Alli P (S n) tl
  IHX : Alli Q (S n) tl → Alli (Trel_conj P Q) (S n) tl
  X0 : Q n hd
  X1 : Alli Q (S n) tl
  ============================
   (P n hd × Q n hd)

  
  A : Type
  P : nat → A → Type
  Q : nat → A → Type
  n : nat
  hd : A
  tl : list A
  p : P n hd
  X : Alli P (S n) tl
  IHX : Alli Q (S n) tl → Alli (Trel_conj P Q) (S n) tl
  X0 : Q n hd
  X1 : Alli Q (S n) tl
  ============================
   (Alli (Trel_conj P Q) (S n) tl)


DEBUG:Going to execute:
auto

Goals:
  
  A : Type
  P : nat → A → Type
  Q : nat → A → Type
  n : nat
  hd : A
  tl : list A
  p : P n hd
  X : Alli P (S n) tl
  IHX : Alli Q (S n) tl → Alli (Trel_conj P Q) (S n) tl
  X0 : Q n hd
  X1 : Alli Q (S n) tl
  ============================
   (P n hd × Q n hd)

  
  A : Type
  P : nat → A → Type
  Q : nat → A → Type
  n : nat
  hd : A
  tl : list A
  p : P n hd
  X : Alli P (S n) tl
  IHX : Alli Q (S n) tl → Alli (Trel_conj P Q) (S n) tl
  X0 : Q n hd
  X1 : Alli Q (S n) tl
  ============================
   (Alli (Trel_conj P Q) (S n) tl)


DEBUG:Going to execute:
<coq-core.plugins.ltac::auto@0> $1 $2 $3