Goal:
  
  A : Type
  B : Type
  p : A → B → bool
  l : list A
  l' : list B
  q : list A
  q' : list B
  ============================
   (forallb2 p l l' && forallb2 p q q' → forallb2 p (l ++ q) (l' ++ q'))


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

Goals:
  
  A : Type
  B : Type
  p : A → B → bool
  l' : list B
  q : list A
  q' : list B
  ============================
   (forallb2 p [] l' && forallb2 p q q' → forallb2 p ([] ++ q) (l' ++ q'))

  
  A : Type
  B : Type
  p : A → B → bool
  a : A
  l : list A
  l' : list B
  q : list A
  q' : list B
  IHl : ∀ l' : list B,
          forallb2 p l l' && forallb2 p q q' → forallb2 p (l ++ q) (l' ++ q')
  ============================
   (forallb2 p (a :: l) l' && forallb2 p q q'
    → forallb2 p ((a :: l) ++ q) (l' ++ q'))


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

Goals:
    A : Type  B : Type  p : A → B → bool  q : list A  q' : list B
  ============================
   (forallb2 p [] [] && forallb2 p q q' → forallb2 p ([] ++ q) ([] ++ q'))

  
  A : Type
  B : Type
  p : A → B → bool
  b : B
  l' : list B
  q : list A
  q' : list B
  ============================
   (forallb2 p [] (b :: l') && forallb2 p q q'
    → forallb2 p ([] ++ q) ((b :: l') ++ q'))

  
  A : Type
  B : Type
  p : A → B → bool
  a : A
  l : list A
  q : list A
  q' : list B
  IHl : ∀ l' : list B,
          forallb2 p l l' && forallb2 p q q' → forallb2 p (l ++ q) (l' ++ q')
  ============================
   (forallb2 p (a :: l) [] && forallb2 p q q'
    → forallb2 p ((a :: l) ++ q) ([] ++ q'))

  
  A : Type
  B : Type
  p : A → B → bool
  a : A
  l : list A
  b : B
  l' : list B
  q : list A
  q' : list B
  IHl : ∀ l' : list B,
          forallb2 p l l' && forallb2 p q q' → forallb2 p (l ++ q) (l' ++ q')
  ============================
   (forallb2 p (a :: l) (b :: l') && forallb2 p q q'
    → forallb2 p ((a :: l) ++ q) ((b :: l') ++ q'))


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

Goals:
    A : Type  B : Type  p : A → B → bool  q : list A  q' : list B
  ============================
   (forallb2 p q q' → forallb2 p q q')

  
  A : Type
  B : Type
  p : A → B → bool
  b : B
  l' : list B
  q : list A
  q' : list B
  ============================
   (false → forallb2 p q (b :: l' ++ q'))

  
  A : Type
  B : Type
  p : A → B → bool
  a : A
  l : list A
  q : list A
  q' : list B
  IHl : ∀ l' : list B,
          forallb2 p l l' && forallb2 p q q' → forallb2 p (l ++ q) (l' ++ q')
  ============================
   (false
    → match q' with
      | [] => false
      | hd' :: tl' => p a hd' && forallb2 p (l ++ q) tl'
      end)

  
  A : Type
  B : Type
  p : A → B → bool
  a : A
  l : list A
  b : B
  l' : list B
  q : list A
  q' : list B
  IHl : ∀ l' : list B,
          forallb2 p l l' && forallb2 p q q' → forallb2 p (l ++ q) (l' ++ q')
  ============================
   (p a b && forallb2 p l l' && forallb2 p q q'
    → p a b && forallb2 p (l ++ q) (l' ++ q'))


DEBUG:Going to execute:
try congruence