Goal:
    A : Type  P : A → Prop  Q : A → Prop  l : list A  l' : list A
  ============================
   (All P l → All Q l' → #|l| = #|l'| → All2 (λ x y : A, P x ∧ Q y) l l')


DEBUG:Going to execute:
induction l in l' |- *

Goals:
    A : Type  P : A → Prop  Q : A → Prop  l' : list A
  ============================
   (All P [] → All Q l' → #|[]| = #|l'| → All2 (λ x y : A, P x ∧ Q y) [] l')

  
  A : Type
  P : A → Prop
  Q : A → Prop
  a : A
  l : list A
  l' : list A
  IHl : ∀ l' : list A,
          All P l
          → All Q l' → #|l| = #|l'| → All2 (λ x y : A, P x ∧ Q y) l l'
  ============================
   (All P (a :: l)
    → All Q l' → #|a :: l| = #|l'| → All2 (λ x y : A, P x ∧ Q y) (a :: l) l')


DEBUG:Going to execute:
destruct l'
DEBUG LTAC Evaluated term: l

Goals:
    A : Type  P : A → Prop  Q : A → Prop
  ============================
   (All P [] → All Q [] → #|[]| = #|[]| → All2 (λ x y : A, P x ∧ Q y) [] [])

    A : Type  P : A → Prop  Q : A → Prop  a : A  l' : list A
  ============================
   (All P []
    → All Q (a :: l')
      → #|[]| = #|a :: l'| → All2 (λ x y : A, P x ∧ Q y) [] (a :: l'))

  
  A : Type
  P : A → Prop
  Q : A → Prop
  a : A
  l : list A
  IHl : ∀ l' : list A,
          All P l
          → All Q l' → #|l| = #|l'| → All2 (λ x y : A, P x ∧ Q y) l l'
  ============================
   (All P (a :: l)
    → All Q [] → #|a :: l| = #|[]| → All2 (λ x y : A, P x ∧ Q y) (a :: l) [])

  
  A : Type
  P : A → Prop
  Q : A → Prop
  a : A
  l : list A
  a0 : A
  l' : list A
  IHl : ∀ l' : list A,
          All P l
          → All Q l' → #|l| = #|l'| → All2 (λ x y : A, P x ∧ Q y) l l'
  ============================
   (All P (a :: l)
    → All Q (a0 :: l')
      → #|a :: l| = #|a0 :: l'|
        → All2 (λ x y : A, P x ∧ Q y) (a :: l) (a0 :: l'))


DEBUG:Going to execute:
simpl
DEBUG LTAC Evaluated term: l'
DEBUG LTAC Evaluated term: l'

Goals:
    A : Type  P : A → Prop  Q : A → Prop
  ============================
   (All P [] → All Q [] → 0 = 0 → All2 (λ x y : A, P x ∧ Q y) [] [])

    A : Type  P : A → Prop  Q : A → Prop  a : A  l' : list A
  ============================
   (All P []
    → All Q (a :: l')
      → 0 = S #|l'| → All2 (λ x y : A, P x ∧ Q y) [] (a :: l'))

  
  A : Type
  P : A → Prop
  Q : A → Prop
  a : A
  l : list A
  IHl : ∀ l' : list A,
          All P l
          → All Q l' → #|l| = #|l'| → All2 (λ x y : A, P x ∧ Q y) l l'
  ============================
   (All P (a :: l)
    → All Q [] → S #|l| = 0 → All2 (λ x y : A, P x ∧ Q y) (a :: l) [])

  
  A : Type
  P : A → Prop
  Q : A → Prop
  a : A
  l : list A
  a0 : A
  l' : list A
  IHl : ∀ l' : list A,
          All P l
          → All Q l' → #|l| = #|l'| → All2 (λ x y : A, P x ∧ Q y) l l'
  ============================
   (All P (a :: l)
    → All Q (a0 :: l')
      → S #|l| = S #|l'| → All2 (λ x y : A, P x ∧ Q y) (a :: l) (a0 :: l'))


DEBUG:Going to execute:
auto => //