Goal:
  
  A : Type
  B : Type
  P : A → Type
  Q : A → B → Type
  b : B
  l' : list B
  x : A
  l : list A
  p : P x
  H1 : All P l
  H2 : ∀ (x : A) (y : B), In y (b :: l') → P x → Q x y
  H : #|l| = #|l'|
  IHAll : ∀ l' : list B,
            (∀ (x : A) (y : B), In y l' → P x → Q x y)
            → #|l'| = #|l| → All2 Q l l'
  ============================
   (All2 Q (x :: l) (b :: l'))


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

Goals:
  
  A : Type
  B : Type
  P : A → Type
  Q : A → B → Type
  b : B
  l' : list B
  x : A
  l : list A
  p : P x
  H1 : All P l
  H2 : ∀ (x : A) (y : B), In y (b :: l') → P x → Q x y
  H : #|l| = #|l'|
  IHAll : ∀ l' : list B,
            (∀ (x : A) (y : B), In y l' → P x → Q x y)
            → #|l'| = #|l| → All2 Q l l'
  ============================
   (Q x b)

  
  A : Type
  B : Type
  P : A → Type
  Q : A → B → Type
  b : B
  l' : list B
  x : A
  l : list A
  p : P x
  H1 : All P l
  H2 : ∀ (x : A) (y : B), In y (b :: l') → P x → Q x y
  H : #|l| = #|l'|
  IHAll : ∀ l' : list B,
            (∀ (x : A) (y : B), In y l' → P x → Q x y)
            → #|l'| = #|l| → All2 Q l l'
  ============================
   (All2 Q l l')


DEBUG:Going to execute:
firstorder

Goals:
  
  A : Type
  B : Type
  P : A → Type
  Q : A → B → Type
  b : B
  l' : list B
  x : A
  l : list A
  p : P x
  H1 : All P l
  H2 : ∀ (x : A) (y : B), In y (b :: l') → P x → Q x y
  H : #|l| = #|l'|
  IHAll : ∀ l' : list B,
            (∀ (x : A) (y : B), In y l' → P x → Q x y)
            → #|l'| = #|l| → All2 Q l l'
  ============================
   (Q x b)

  
  A : Type
  B : Type
  P : A → Type
  Q : A → B → Type
  b : B
  l' : list B
  x : A
  l : list A
  p : P x
  H1 : All P l
  H2 : ∀ (x : A) (y : B), In y (b :: l') → P x → Q x y
  H : #|l| = #|l'|
  IHAll : ∀ l' : list B,
            (∀ (x : A) (y : B), In y l' → P x → Q x y)
            → #|l'| = #|l| → All2 Q l l'
  ============================
   (All2 Q l l')


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

Debug:
  
  A : Type
  B : Type
  P : A → Type
  Q : A → B → Type
  b : B
  l' : list B
  x : A
  l : list A
  p : P x
  H1 : All P l
  H2 : ∀ (x : A) (y : B), In y (b :: l') → P x → Q x y
  H : #|l| = #|l'|
  IHAll : ∀ l' : list B,
            (∀ (x : A) (y : B), In y l' → P x → Q x y)
            → #|l'| = #|l| → All2 Q l l'
  ============================
  Q x b
Debug:
  
  A : Type
  B : Type
  P : A → Type
  Q : A → B → Type
  b : B
  l' : list B
  x : A
  l : list A
  p : P x
  H1 : All P l
  H2 : ∀ (x : A) (y : B), In y (b :: l') → P x → Q x y
  H : #|l| = #|l'|
  IHAll : ∀ l' : list B,
            (∀ (x : A) (y : B), In y l' → P x → Q x y)
            → #|l'| = #|l| → All2 Q l l'
  X : ∀ y : B, In y (b :: l') → P x → Q x y
  ============================
  Q x b
Debug:
  
  A : Type
  B : Type
  P : A → Type
  Q : A → B → Type
  b : B
  l' : list B
  x : A
  l : list A
  p : P x
  H1 : All P l
  H2 : ∀ (x : A) (y : B), In y (b :: l') → P x → Q x y
  H : #|l| = #|l'|
  IHAll : ∀ l' : list B,
            (∀ (x : A) (y : B), In y l' → P x → Q x y)
            → #|l'| = #|l| → All2 Q l l'
  X : ∀ y : B, In y (b :: l') → P x → Q x y
  X0 : (∀ (x : A) (y : B), In y l' → P x → Q x y)
       → #|l'| = #|l| → All2 Q l l'
  ============================
  Q x b
Debug:
  
  A : Type
  B : Type
  P : A → Type
  Q : A → B → Type
  b : B
  l' : list B
  x : A
  l : list A
  p : P x
  H1 : All P l
  H2 : ∀ (x : A) (y : B), In y (b :: l') → P x → Q x y
  H : #|l| = #|l'|
  IHAll : ∀ l' : list B,
            (∀ (x : A) (y : B), In y l' → P x → Q x y)
            → #|l'| = #|l| → All2 Q l l'
  X : ∀ y : B, In y (b :: l') → P x → Q x y
  X0 : #|l'| = #|l| → All2 Q l l'
  ============================
  Q x b
Debug:
  
  A : Type
  B : Type
  P : A → Type
  Q : A → B → Type
  b : B
  l' : list B
  x : A
  l : list A
  p : P x
  H1 : All P l
  H2 : ∀ (x : A) (y : B), In y (b :: l') → P x → Q x y
  H : #|l| = #|l'|
  IHAll : ∀ l' : list B,
            (∀ (x : A) (y : B), In y l' → P x → Q x y)
            → #|l'| = #|l| → All2 Q l l'
  X : ∀ y : B, In y (b :: l') → P x → Q x y
  X0 : #|l'| = #|l| → All2 Q l l'
  ============================
  Q x b
Debug:
  
  A : Type
  B : Type
  P : A → Type
  Q : A → B → Type
  b : B
  l' : list B
  x : A
  l : list A
  p : P x
  H1 : All P l
  H2 : ∀ (x : A) (y : B), In y (b :: l') → P x → Q x y
  H : #|l| = #|l'|
  IHAll : ∀ l' : list B,
            (∀ (x : A) (y : B), In y l' → P x → Q x y)
            → #|l'| = #|l| → All2 Q l l'
  X : ∀ y : B, In y (b :: l') → P x → Q x y
  X0 : #|l'| = #|l| → All2 Q l l'
  ============================
  Q x b
Debug:
  
  A : Type
  B : Type
  P : A → Type
  Q : A → B → Type
  b : B
  l' : list B
  x : A
  l : list A
  p : P x
  H1 : All P l
  H2 : ∀ (x : A) (y : B), In y (b :: l') → P x → Q x y
  H : #|l| = #|l'|
  IHAll : ∀ l' : list B,
            (∀ (x : A) (y : B), In y l' → P x → Q x y)
            → #|l'| = #|l| → All2 Q l l'
  X : ∀ y : B, In y (b :: l') → P x → Q x y
  X0 : (∀ (x : A) (y : B), In y l' → P x → Q x y)
       → #|l'| = #|l| → All2 Q l l'
  ============================
  Q x b
Debug:
  
  A : Type
  B : Type
  P : A → Type
  Q : A → B → Type
  b : B
  l' : list B
  x : A
  l : list A
  p : P x
  H1 : All P l
  H2 : ∀ (x : A) (y : B), In y (b :: l') → P x → Q x y
  H : #|l| = #|l'|
  IHAll : ∀ l' : list B,
            (∀ (x : A) (y : B), In y l' → P x → Q x y)
            → #|l'| = #|l| → All2 Q l l'
  X : ∀ y : B, In y (b :: l') → P x → Q x y
  X0 : (∀ (x : A) (y : B), In y l' → P x → Q x y)
       → #|l'| = #|l| → All2 Q l l'
  X1 : In b (b :: l') → P x → Q x b
  ============================
  Q x b
Debug:
  
  A : Type
  B : Type
  P : A → Type
  Q : A → B → Type
  b : B
  l' : list B
  x : A
  l : list A
  p : P x
  H1 : All P l
  H2 : ∀ (x : A) (y : B), In y (b :: l') → P x → Q x y
  H : #|l| = #|l'|
  IHAll : ∀ l' : list B,
            (∀ (x : A) (y : B), In y l' → P x → Q x y)
            → #|l'| = #|l| → All2 Q l l'
  X : ∀ y : B, In y (b :: l') → P x → Q x y
  X0 : (∀ (x : A) (y : B), In y l' → P x → Q x y)
       → #|l'| = #|l| → All2 Q l l'
  X1 : b = b → P x → Q x b
  X2 : (fix In (a : B) (l : list B) {struct l} : Prop :=
          match l with
          | [] => False
          | b :: m => b = a ∨ In a m
          end) b l' → P x → Q x b
  ============================
  Q x b
Debug:
  
  A : Type
  B : Type
  P : A → Type
  Q : A → B → Type
  b : B
  l' : list B
  x : A
  l : list A
  p : P x
  H1 : All P l
  H2 : ∀ (x : A) (y : B), In y (b :: l') → P x → Q x y
  H : #|l| = #|l'|
  IHAll : ∀ l' : list B,
            (∀ (x : A) (y : B), In y l' → P x → Q x y)
            → #|l'| = #|l| → All2 Q l l'
  X : ∀ y : B, In y (b :: l') → P x → Q x y
  X0 : (∀ (x : A) (y : B), In y l' → P x → Q x y)
       → #|l'| = #|l| → All2 Q l l'
  X2 : (fix In (a : B) (l : list B) {struct l} : Prop :=
          match l with
          | [] => False
          | b :: m => b = a ∨ In a m
          end) b l' → P x → Q x b
  X1 : P x → Q x b
  ============================
  Q x b
Debug:
  
  A : Type
  B : Type
  P : A → Type
  Q : A → B → Type
  b : B
  l' : list B
  x : A
  l : list A
  p : P x
  H1 : All P l
  H2 : ∀ (x : A) (y : B), In y (b :: l') → P x → Q x y
  H : #|l| = #|l'|
  IHAll : ∀ l' : list B,
            (∀ (x : A) (y : B), In y l' → P x → Q x y)
            → #|l'| = #|l| → All2 Q l l'
  X : ∀ y : B, In y (b :: l') → P x → Q x y
  X0 : (∀ (x : A) (y : B), In y l' → P x → Q x y)
       → #|l'| = #|l| → All2 Q l l'
  X2 : (fix In (a : B) (l : list B) {struct l} : Prop :=
          match l with
          | [] => False
          | b :: m => b = a ∨ In a m
          end) b l' → P x → Q x b
  X1 : Q x b
  ============================
  Q x b
Debug:
  
  A : Type
  B : Type
  P : A → Type
  Q : A → B → Type
  b : B
  l' : list B
  x : A
  l : list A
  p : P x
  H1 : All P l
  H2 : ∀ (x : A) (y : B), In y (b :: l') → P x → Q x y
  H : #|l| = #|l'|
  IHAll : ∀ l' : list B,
            (∀ (x : A) (y : B), In y l' → P x → Q x y)
            → #|l'| = #|l| → All2 Q l l'
  ============================
  All2 Q l l'
Debug:
  
  A : Type
  B : Type
  P : A → Type
  Q : A → B → Type
  b : B
  l' : list B
  x : A
  l : list A
  p : P x
  H1 : All P l
  H2 : ∀ (x : A) (y : B), In y (b :: l') → P x → Q x y
  H : #|l| = #|l'|
  IHAll : ∀ l' : list B,
            (∀ (x : A) (y : B), In y l' → P x → Q x y)
            → #|l'| = #|l| → All2 Q l l'
  X : ∀ y : B, In y (b :: l') → P x → Q x y
  ============================
  All2 Q l l'
Debug:
  
  A : Type
  B : Type
  P : A → Type
  Q : A → B → Type
  b : B
  l' : list B
  x : A
  l : list A
  p : P x
  H1 : All P l
  H2 : ∀ (x : A) (y : B), In y (b :: l') → P x → Q x y
  H : #|l| = #|l'|
  IHAll : ∀ l' : list B,
            (∀ (x : A) (y : B), In y l' → P x → Q x y)
            → #|l'| = #|l| → All2 Q l l'
  X : ∀ y : B, In y (b :: l') → P x → Q x y
  X0 : (∀ (x : A) (y : B), In y l' → P x → Q x y)
       → #|l'| = #|l| → All2 Q l l'
  ============================
  All2 Q l l'
Debug:
  
  A : Type
  B : Type
  P : A → Type
  Q : A → B → Type
  b : B
  l' : list B
  x : A
  l : list A
  p : P x
  H1 : All P l
  H2 : ∀ (x : A) (y : B), In y (b :: l') → P x → Q x y
  H : #|l| = #|l'|
  IHAll : ∀ l' : list B,
            (∀ (x : A) (y : B), In y l' → P x → Q x y)
            → #|l'| = #|l| → All2 Q l l'
  X : ∀ y : B, In y (b :: l') → P x → Q x y
  X0 : #|l'| = #|l| → All2 Q l l'
  ============================
  All2 Q l l'
Debug:
  
  A : Type
  B : Type
  P : A → Type
  Q : A → B → Type
  b : B
  l' : list B
  x : A
  l : list A
  p : P x
  H1 : All P l
  H2 : ∀ (x : A) (y : B), In y (b :: l') → P x → Q x y
  H : #|l| = #|l'|
  IHAll : ∀ l' : list B,
            (∀ (x : A) (y : B), In y l' → P x → Q x y)
            → #|l'| = #|l| → All2 Q l l'
  X : ∀ y : B, In y (b :: l') → P x → Q x y
  X0 : #|l'| = #|l| → All2 Q l l'
  ============================
  All2 Q l l'
Debug:
  
  A : Type
  B : Type
  P : A → Type
  Q : A → B → Type
  b : B
  l' : list B
  x : A
  l : list A
  p : P x
  H1 : All P l
  H2 : ∀ (x : A) (y : B), In y (b :: l') → P x → Q x y
  H : #|l| = #|l'|
  IHAll : ∀ l' : list B,
            (∀ (x : A) (y : B), In y l' → P x → Q x y)
            → #|l'| = #|l| → All2 Q l l'
  X : ∀ y : B, In y (b :: l') → P x → Q x y
  X0 : #|l'| = #|l| → All2 Q l l'
  ============================
  All2 Q l l'
Debug:
  
  A : Type
  B : Type
  P : A → Type
  Q : A → B → Type
  b : B
  l' : list B
  x : A
  l : list A
  p : P x
  H1 : All P l
  H2 : ∀ (x : A) (y : B), In y (b :: l') → P x → Q x y
  H : #|l| = #|l'|
  IHAll : ∀ l' : list B,
            (∀ (x : A) (y : B), In y l' → P x → Q x y)
            → #|l'| = #|l| → All2 Q l l'
  X : ∀ y : B, In y (b :: l') → P x → Q x y
  X0 : (∀ (x : A) (y : B), In y l' → P x → Q x y)
       → #|l'| = #|l| → All2 Q l l'
  ============================
  ∀ (x0 : A) (y : B), In y l' → P x0 → Q x0 y
Debug:
  
  A : Type
  B : Type
  P : A → Type
  Q : A → B → Type
  b : B
  l' : list B
  x : A
  l : list A
  p : P x
  H1 : All P l
  H2 : ∀ (x : A) (y : B), In y (b :: l') → P x → Q x y
  H : #|l| = #|l'|
  IHAll : ∀ l' : list B,
            (∀ (x : A) (y : B), In y l' → P x → Q x y)
            → #|l'| = #|l| → All2 Q l l'
  X : ∀ y : B, In y (b :: l') → P x → Q x y
  X0 : (∀ (x : A) (y : B), In y l' → P x → Q x y)
       → #|l'| = #|l| → All2 Q l l'
  x0 : A
  ============================
  ∀ y : B, In y l' → P x0 → Q x0 y
Debug:
  
  A : Type
  B : Type
  P : A → Type
  Q : A → B → Type
  b : B
  l' : list B
  x : A
  l : list A
  p : P x
  H1 : All P l
  H2 : ∀ (x : A) (y : B), In y (b :: l') → P x → Q x y
  H : #|l| = #|l'|
  IHAll : ∀ l' : list B,
            (∀ (x : A) (y : B), In y l' → P x → Q x y)
            → #|l'| = #|l| → All2 Q l l'
  X : ∀ y : B, In y (b :: l') → P x → Q x y
  X0 : (∀ (x : A) (y : B), In y l' → P x → Q x y)
       → #|l'| = #|l| → All2 Q l l'
  x0 : A
  y : B
  ============================
  In y l' → P x0 → Q x0 y
Debug:
  
  A : Type
  B : Type
  P : A → Type
  Q : A → B → Type
  b : B
  l' : list B
  x : A
  l : list A
  p : P x
  H1 : All P l
  H2 : ∀ (x : A) (y : B), In y (b :: l') → P x → Q x y
  H : #|l| = #|l'|
  IHAll : ∀ l' : list B,
            (∀ (x : A) (y : B), In y l' → P x → Q x y)
            → #|l'| = #|l| → All2 Q l l'
  X : ∀ y : B, In y (b :: l') → P x → Q x y
  X0 : (∀ (x : A) (y : B), In y l' → P x → Q x y)
       → #|l'| = #|l| → All2 Q l l'
  x0 : A
  y : B
  H0 : In y l'
  ============================
  P x0 → Q x0 y
Debug:
  
  A : Type
  B : Type
  P : A → Type
  Q : A → B → Type
  b : B
  l' : list B
  x : A
  l : list A
  p : P x
  H1 : All P l
  H2 : ∀ (x : A) (y : B), In y (b :: l') → P x → Q x y
  H : #|l| = #|l'|
  IHAll : ∀ l' : list B,
            (∀ (x : A) (y : B), In y l' → P x → Q x y)
            → #|l'| = #|l| → All2 Q l l'
  X : ∀ y : B, In y (b :: l') → P x → Q x y
  X0 : (∀ (x : A) (y : B), In y l' → P x → Q x y)
       → #|l'| = #|l| → All2 Q l l'
  x0 : A
  y : B
  H0 : In y l'
  X1 : P x0
  ============================
  Q x0 y
Debug:
  
  A : Type
  B : Type
  P : A → Type
  Q : A → B → Type
  b : B
  l' : list B
  x : A
  l : list A
  p : P x
  H1 : All P l
  H2 : ∀ (x : A) (y : B), In y (b :: l') → P x → Q x y
  H : #|l| = #|l'|
  IHAll : ∀ l' : list B,
            (∀ (x : A) (y : B), In y l' → P x → Q x y)
            → #|l'| = #|l| → All2 Q l l'
  X : ∀ y : B, In y (b :: l') → P x → Q x y
  X0 : (∀ (x : A) (y : B), In y l' → P x → Q x y)
       → #|l'| = #|l| → All2 Q l l'
  x0 : A
  y : B
  H0 : In y l'
  X1 : P x0
  ============================
  Q x0 y
Debug:
  
  A : Type
  B : Type
  P : A → Type
  Q : A → B → Type
  b : B
  l' : list B
  x : A
  l : list A
  p : P x
  H1 : All P l
  H2 : ∀ (x : A) (y : B), In y (b :: l') → P x → Q x y
  H : #|l| = #|l'|
  IHAll : ∀ l' : list B,
            (∀ (x : A) (y : B), In y l' → P x → Q x y)
            → #|l'| = #|l| → All2 Q l l'
  X : ∀ y : B, In y (b :: l') → P x → Q x y
  X0 : (∀ (x : A) (y : B), In y l' → P x → Q x y)
       → #|l'| = #|l| → All2 Q l l'
  ============================
  All2 Q l l'
Debug:
  
  A : Type
  B : Type
  P : A → Type
  Q : A → B → Type
  b : B
  l' : list B
  x : A
  l : list A
  p : P x
  H1 : All P l
  H2 : ∀ (x : A) (y : B), In y (b :: l') → P x → Q x y
  H : #|l| = #|l'|
  IHAll : ∀ l' : list B,
            (∀ (x : A) (y : B), In y l' → P x → Q x y)
            → #|l'| = #|l| → All2 Q l l'
  X : ∀ y : B, In y (b :: l') → P x → Q x y
  X0 : (∀ (x : A) (y : B), In y l' → P x → Q x y)
       → #|l'| = #|l| → All2 Q l l'
  X1 : B
  X2 : In X1 (b :: l') → P x → Q x X1
  ============================
  All2 Q l l'
Debug:
  
  A : Type
  B : Type
  P : A → Type
  Q : A → B → Type
  b : B
  l' : list B
  x : A
  l : list A
  p : P x
  H1 : All P l
  H2 : ∀ (x : A) (y : B), In y (b :: l') → P x → Q x y
  H : #|l| = #|l'|
  IHAll : ∀ l' : list B,
            (∀ (x : A) (y : B), In y l' → P x → Q x y)
            → #|l'| = #|l| → All2 Q l l'
  X : ∀ y : B, In y (b :: l') → P x → Q x y
  X0 : (∀ (x : A) (y : B), In y l' → P x → Q x y)
       → #|l'| = #|l| → All2 Q l l'
  X1 : B
  X2 : b = X1 → P x → Q x X1
  X3 : (fix In (a : B) (l : list B) {struct l} : Prop :=
          match l with
          | [] => False
          | b :: m => b = a ∨ In a m
          end) X1 l' → P x → Q x X1
  ============================
  All2 Q l l'
Debug:
  
  A : Type
  B : Type
  P : A → Type
  Q : A → B → Type
  b : B
  l' : list B
  x : A
  l : list A
  p : P x
  H1 : All P l
  H2 : ∀ (x : A) (y : B), In y (b :: l') → P x → Q x y
  H : #|l| = #|l'|
  IHAll : ∀ l' : list B,
            (∀ (x : A) (y : B), In y l' → P x → Q x y)
            → #|l'| = #|l| → All2 Q l l'
  X : ∀ y : B, In y (b :: l') → P x → Q x y
  X0 : (∀ (x : A) (y : B), In y l' → P x → Q x y)
       → #|l'| = #|l| → All2 Q l l'
  X1 : B
  X2 : b = X1 → P x → Q x X1
  X3 : (fix In (a : B) (l : list B) {struct l} : Prop :=
          match l with
          | [] => False
          | b :: m => b = a ∨ In a m
          end) X1 l' → P x → Q x X1
  ============================
  All2 Q l l'
Debug:
  
  A : Type
  B : Type
  P : A → Type
  Q : A → B → Type
  b : B
  l' : list B
  x : A
  l : list A
  p : P x
  H1 : All P l
  H2 : ∀ (x : A) (y : B), In y (b :: l') → P x → Q x y
  H : #|l| = #|l'|
  IHAll : ∀ l' : list B,
            (∀ (x : A) (y : B), In y l' → P x → Q x y)
            → #|l'| = #|l| → All2 Q l l'
  X : ∀ y : B, In y (b :: l') → P x → Q x y
  X0 : (∀ (x : A) (y : B), In y l' → P x → Q x y)
       → #|l'| = #|l| → All2 Q l l'
  X1 : B
  X2 : b = X1 → P x → Q x X1
  X3 : (fix In (a : B) (l : list B) {struct l} : Prop :=
          match l with
          | [] => False
          | b :: m => b = a ∨ In a m
          end) X1 l' → P x → Q x X1
  ============================
  All2 Q l l'
Debug:
  
  A : Type
  B : Type
  P : A → Type
  Q : A → B → Type
  b : B
  l' : list B
  x : A
  l : list A
  p : P x
  H1 : All P l
  H2 : ∀ (x : A) (y : B), In y (b :: l') → P x → Q x y
  H : #|l| = #|l'|
  IHAll : ∀ l' : list B,
            (∀ (x : A) (y : B), In y l' → P x → Q x y)
            → #|l'| = #|l| → All2 Q l l'
  X : ∀ y : B, In y (b :: l') → P x → Q x y
  X0 : (∀ (x : A) (y : B), In y l' → P x → Q x y)
       → #|l'| = #|l| → All2 Q l l'
  X1 : B
  X2 : b = X1 → P x → Q x X1
  X3 : (fix In (a : B) (l : list B) {struct l} : Prop :=
          match l with
          | [] => False
          | b :: m => b = a ∨ In a m
          end) X1 l' → P x → Q x X1
  ============================
  All2 Q l l'
Debug:
  
  A : Type
  B : Type
  P : A → Type
  Q : A → B → Type
  b : B
  l' : list B
  x : A
  l : list A
  p : P x
  H1 : All P l
  H2 : ∀ (x : A) (y : B), In y (b :: l') → P x → Q x y
  H : #|l| = #|l'|
  IHAll : ∀ l' : list B,
            (∀ (x : A) (y : B), In y l' → P x → Q x y)
            → #|l'| = #|l| → All2 Q l l'
  X : ∀ y : B, In y (b :: l') → P x → Q x y
  X0 : (∀ (x : A) (y : B), In y l' → P x → Q x y)
       → #|l'| = #|l| → All2 Q l l'
  X1 : B
  X2 : b = X1 → P x → Q x X1
  X3 : (fix In (a : B) (l : list B) {struct l} : Prop :=
          match l with
          | [] => False
          | b :: m => b = a ∨ In a m
          end) X1 l' → P x → Q x X1
  ============================
  All2 Q l l'
Debug:
  
  A : Type
  B : Type
  P : A → Type
  Q : A → B → Type
  b : B
  l' : list B
  x : A
  l : list A
  p : P x
  H1 : All P l
  H2 : ∀ (x : A) (y : B), In y (b :: l') → P x → Q x y
  H : #|l| = #|l'|
  IHAll : ∀ l' : list B,
            (∀ (x : A) (y : B), In y l' → P x → Q x y)
            → #|l'| = #|l| → All2 Q l l'
  X : ∀ y : B, In y (b :: l') → P x → Q x y
  X0 : (∀ (x : A) (y : B), In y l' → P x → Q x y)
       → #|l'| = #|l| → All2 Q l l'
  ============================
  All2 Q l l'
Debug:
  
  A : Type
  B : Type
  P : A → Type
  Q : A → B → Type
  b : B
  l' : list B
  x : A
  l : list A
  p : P x
  H1 : All P l
  H2 : ∀ (x : A) (y : B), In y (b :: l') → P x → Q x y
  H : #|l| = #|l'|
  IHAll : ∀ l' : list B,
            (∀ (x : A) (y : B), In y l' → P x → Q x y)
            → #|l'| = #|l| → All2 Q l l'
  X : ∀ y : B, In y (b :: l') → P x → Q x y
  X0 : B
  X1 : In X0 (b :: l') → P x → Q x X0
  ============================
  All2 Q l l'
Debug:
  
  A : Type
  B : Type
  P : A → Type
  Q : A → B → Type
  b : B
  l' : list B
  x : A
  l : list A
  p : P x
  H1 : All P l
  H2 : ∀ (x : A) (y : B), In y (b :: l') → P x → Q x y
  H : #|l| = #|l'|
  IHAll : ∀ l' : list B,
            (∀ (x : A) (y : B), In y l' → P x → Q x y)
            → #|l'| = #|l| → All2 Q l l'
  X : ∀ y : B, In y (b :: l') → P x → Q x y
  X0 : B
  X1 : b = X0 → P x → Q x X0
  X2 : (fix In (a : B) (l : list B) {struct l} : Prop :=
          match l with
          | [] => False
          | b :: m => b = a ∨ In a m
          end) X0 l' → P x → Q x X0
  ============================
  All2 Q l l'
Debug:
  
  A : Type
  B : Type
  P : A → Type
  Q : A → B → Type
  b : B
  l' : list B
  x : A
  l : list A
  p : P x
  H1 : All P l
  H2 : ∀ (x : A) (y : B), In y (b :: l') → P x → Q x y
  H : #|l| = #|l'|
  IHAll : ∀ l' : list B,
            (∀ (x : A) (y : B), In y l' → P x → Q x y)
            → #|l'| = #|l| → All2 Q l l'
  X : ∀ y : B, In y (b :: l') → P x → Q x y
  X0 : B
  X1 : b = X0 → P x → Q x X0
  X2 : (fix In (a : B) (l : list B) {struct l} : Prop :=
          match l with
          | [] => False
          | b :: m => b = a ∨ In a m
          end) X0 l' → P x → Q x X0
  ============================
  All2 Q l l'
Debug:
  
  A : Type
  B : Type
  P : A → Type
  Q : A → B → Type
  b : B
  l' : list B
  x : A
  l : list A
  p : P x
  H1 : All P l
  H2 : ∀ (x : A) (y : B), In y (b :: l') → P x → Q x y
  H : #|l| = #|l'|
  IHAll : ∀ l' : list B,
            (∀ (x : A) (y : B), In y l' → P x → Q x y)
            → #|l'| = #|l| → All2 Q l l'
  X : ∀ y : B, In y (b :: l') → P x → Q x y
  X0 : B
  X1 : b = X0 → P x → Q x X0
  X2 : (fix In (a : B) (l : list B) {struct l} : Prop :=
          match l with
          | [] => False
          | b :: m => b = a ∨ In a m
          end) X0 l' → P x → Q x X0
  ============================
  All2 Q l l'
Debug:
  
  A : Type
  B : Type
  P : A → Type
  Q : A → B → Type
  b : B
  l' : list B
  x : A
  l : list A
  p : P x
  H1 : All P l
  H2 : ∀ (x : A) (y : B), In y (b :: l') → P x → Q x y
  H : #|l| = #|l'|
  IHAll : ∀ l' : list B,
            (∀ (x : A) (y : B), In y l' → P x → Q x y)
            → #|l'| = #|l| → All2 Q l l'
  X : ∀ y : B, In y (b :: l') → P x → Q x y
  X0 : B
  X1 : b = X0 → P x → Q x X0
  X2 : (fix In (a : B) (l : list B) {struct l} : Prop :=
          match l with
          | [] => False
          | b :: m => b = a ∨ In a m
          end) X0 l' → P x → Q x X0
  X3 : (∀ (x : A) (y : B), In y l' → P x → Q x y)
       → #|l'| = #|l| → All2 Q l l'
  ============================
  All2 Q l l'
Debug:
  
  A : Type
  B : Type
  P : A → Type
  Q : A → B → Type
  b : B
  l' : list B
  x : A
  l : list A
  p : P x
  H1 : All P l
  H2 : ∀ (x : A) (y : B), In y (b :: l') → P x → Q x y
  H : #|l| = #|l'|
  IHAll : ∀ l' : list B,
            (∀ (x : A) (y : B), In y l' → P x → Q x y)
            → #|l'| = #|l| → All2 Q l l'
  X : ∀ y : B, In y (b :: l') → P x → Q x y
  X0 : B
  X1 : b = X0 → P x → Q x X0
  X2 : (fix In (a : B) (l : list B) {struct l} : Prop :=
          match l with
          | [] => False
          | b :: m => b = a ∨ In a m
          end) X0 l' → P x → Q x X0
  X3 : (∀ (x : A) (y : B), In y l' → P x → Q x y)
       → #|l'| = #|l| → All2 Q l l'
  ============================
  All2 Q l l'
Debug:
  
  A : Type
  B : Type
  P : A → Type
  Q : A → B → Type
  b : B
  l' : list B
  x : A
  l : list A
  p : P x
  H1 : All P l
  H2 : ∀ (x : A) (y : B), In y (b :: l') → P x → Q x y
  H : #|l| = #|l'|
  IHAll : ∀ l' : list B,
            (∀ (x : A) (y : B), In y l' → P x → Q x y)
            → #|l'| = #|l| → All2 Q l l'
  X : ∀ y : B, In y (b :: l') → P x → Q x y
  X0 : B
  X1 : b = X0 → P x → Q x X0
  X2 : (fix In (a : B) (l : list B) {struct l} : Prop :=
          match l with
          | [] => False
          | b :: m => b = a ∨ In a m
          end) X0 l' → P x → Q x X0
  X3 : (∀ (x : A) (y : B), In y l' → P x → Q x y)
       → #|l'| = #|l| → All2 Q l l'
  ============================
  All2 Q l l'
Debug:
  
  A : Type
  B : Type
  P : A → Type
  Q : A → B → Type
  b : B
  l' : list B
  x : A
  l : list A
  p : P x
  H1 : All P l
  H2 : ∀ (x : A) (y : B), In y (b :: l') → P x → Q x y
  H : #|l| = #|l'|
  IHAll : ∀ l' : list B,
            (∀ (x : A) (y : B), In y l' → P x → Q x y)
            → #|l'| = #|l| → All2 Q l l'
  X : ∀ y : B, In y (b :: l') → P x → Q x y
  X0 : B
  X1 : b = X0 → P x → Q x X0
  X2 : (fix In (a : B) (l : list B) {struct l} : Prop :=
          match l with
          | [] => False
          | b :: m => b = a ∨ In a m
          end) X0 l' → P x → Q x X0
  X3 : (∀ (x : A) (y : B), In y l' → P x → Q x y)
       → #|l'| = #|l| → All2 Q l l'
  ============================
  All2 Q l l'
Debug:
  
  A : Type
  B : Type
  P : A → Type
  Q : A → B → Type
  b : B
  l' : list B
  x : A
  l : list A
  p : P x
  H1 : All P l
  H2 : ∀ (x : A) (y : B), In y (b :: l') → P x → Q x y
  H : #|l| = #|l'|
  IHAll : ∀ l' : list B,
            (∀ (x : A) (y : B), In y l' → P x → Q x y)
            → #|l'| = #|l| → All2 Q l l'
  X : ∀ y : B, In y (b :: l') → P x → Q x y
  X0 : B
  X1 : b = X0 → P x → Q x X0
  X2 : (fix In (a : B) (l : list B) {struct l} : Prop :=
          match l with
          | [] => False
          | b :: m => b = a ∨ In a m
          end) X0 l' → P x → Q x X0
  X3 : (∀ (x : A) (y : B), In y l' → P x → Q x y)
       → #|l'| = #|l| → All2 Q l l'
  ============================
  All2 Q l l'
Debug:
  
  A : Type
  B : Type
  P : A → Type
  Q : A → B → Type
  b : B
  l' : list B
  x : A
  l : list A
  p : P x
  H1 : All P l
  H2 : ∀ (x : A) (y : B), In y (b :: l') → P x → Q x y
  H : #|l| = #|l'|
  IHAll : ∀ l' : list B,
            (∀ (x : A) (y : B), In y l' → P x → Q x y)
            → #|l'| = #|l| → All2 Q l l'
  X : ∀ y : B, In y (b :: l') → P x → Q x y
  X0 : B
  X1 : b = X0 → P x → Q x X0
  X2 : (fix In (a : B) (l : list B) {struct l} : Prop :=
          match l with
          | [] => False
          | b :: m => b = a ∨ In a m
          end) X0 l' → P x → Q x X0
  ============================
  All2 Q l l'
Debug:
  
  A : Type
  B : Type
  P : A → Type
  Q : A → B → Type
  b : B
  l' : list B
  x : A
  l : list A
  p : P x
  H1 : All P l
  H2 : ∀ (x : A) (y : B), In y (b :: l') → P x → Q x y
  H : #|l| = #|l'|
  IHAll : ∀ l' : list B,
            (∀ (x : A) (y : B), In y l' → P x → Q x y)
            → #|l'| = #|l| → All2 Q l l'
  X : ∀ y : B, In y (b :: l') → P x → Q x y
  ============================
  All2 Q l l'
Debug:
  
  A : Type
  B : Type
  P : A → Type
  Q : A → B → Type
  b : B
  l' : list B
  x : A
  l : list A
  p : P x
  H1 : All P l
  H2 : ∀ (x : A) (y : B), In y (b :: l') → P x → Q x y
  H : #|l| = #|l'|
  IHAll : ∀ l' : list B,
            (∀ (x : A) (y : B), In y l' → P x → Q x y)
            → #|l'| = #|l| → All2 Q l l'
  X : (∀ (x : A) (y : B), In y l' → P x → Q x y) → #|l'| = #|l| → All2 Q l l'
  ============================
  All2 Q l l'
Debug:
  
  A : Type
  B : Type
  P : A → Type
  Q : A → B → Type
  b : B
  l' : list B
  x : A
  l : list A
  p : P x
  H1 : All P l
  H2 : ∀ (x : A) (y : B), In y (b :: l') → P x → Q x y
  H : #|l| = #|l'|
  IHAll : ∀ l' : list B,
            (∀ (x : A) (y : B), In y l' → P x → Q x y)
            → #|l'| = #|l| → All2 Q l l'
  X : #|l'| = #|l| → All2 Q l l'
  ============================
  All2 Q l l'
Debug:
  
  A : Type
  B : Type
  P : A → Type
  Q : A → B → Type
  b : B
  l' : list B
  x : A
  l : list A
  p : P x
  H1 : All P l
  H2 : ∀ (x : A) (y : B), In y (b :: l') → P x → Q x y
  H : #|l| = #|l'|
  IHAll : ∀ l' : list B,
            (∀ (x : A) (y : B), In y l' → P x → Q x y)
            → #|l'| = #|l| → All2 Q l l'
  X : #|l'| = #|l| → All2 Q l l'
  ============================
  All2 Q l l'
Debug:
  
  A : Type
  B : Type
  P : A → Type
  Q : A → B → Type
  b : B
  l' : list B
  x : A
  l : list A
  p : P x
  H1 : All P l
  H2 : ∀ (x : A) (y : B), In y (b :: l') → P x → Q x y
  H : #|l| = #|l'|
  IHAll : ∀ l' : list B,
            (∀ (x : A) (y : B), In y l' → P x → Q x y)
            → #|l'| = #|l| → All2 Q l l'
  X : #|l'| = #|l| → All2 Q l l'
  X0 : ∀ y : B, In y (b :: l') → P x → Q x y
  ============================
  All2 Q l l'
Debug:
  
  A : Type
  B : Type
  P : A → Type
  Q : A → B → Type
  b : B
  l' : list B
  x : A
  l : list A
  p : P x
  H1 : All P l
  H2 : ∀ (x : A) (y : B), In y (b :: l') → P x → Q x y
  H : #|l| = #|l'|
  IHAll : ∀ l' : list B,
            (∀ (x : A) (y : B), In y l' → P x → Q x y)
            → #|l'| = #|l| → All2 Q l l'
  X : #|l'| = #|l| → All2 Q l l'
  X0 : ∀ y : B, In y (b :: l') → P x → Q x y
  ============================
  All2 Q l l'
Debug:
  
  A : Type
  B : Type
  P : A → Type
  Q : A → B → Type
  b : B
  l' : list B
  x : A
  l : list A
  p : P x
  H1 : All P l
  H2 : ∀ (x : A) (y : B), In y (b :: l') → P x → Q x y
  H : #|l| = #|l'|
  IHAll : ∀ l' : list B,
            (∀ (x : A) (y : B), In y l' → P x → Q x y)
            → #|l'| = #|l| → All2 Q l l'
  X : #|l'| = #|l| → All2 Q l l'
  X0 : ∀ y : B, In y (b :: l') → P x → Q x y
  ============================
  All2 Q l l'
Debug:
  
  A : Type
  B : Type
  P : A → Type
  Q : A → B → Type
  b : B
  l' : list B
  x : A
  l : list A
  p : P x
  H1 : All P l
  H2 : ∀ (x : A) (y : B), In y (b :: l') → P x → Q x y
  H : #|l| = #|l'|
  IHAll : ∀ l' : list B,
            (∀ (x : A) (y : B), In y l' → P x → Q x y)
            → #|l'| = #|l| → All2 Q l l'
  X : (∀ (x : A) (y : B), In y l' → P x → Q x y) → #|l'| = #|l| → All2 Q l l'
  ============================
  ∀ (x0 : A) (y : B), In y l' → P x0 → Q x0 y
Debug:
  
  A : Type
  B : Type
  P : A → Type
  Q : A → B → Type
  b : B
  l' : list B
  x : A
  l : list A
  p : P x
  H1 : All P l
  H2 : ∀ (x : A) (y : B), In y (b :: l') → P x → Q x y
  H : #|l| = #|l'|
  IHAll : ∀ l' : list B,
            (∀ (x : A) (y : B), In y l' → P x → Q x y)
            → #|l'| = #|l| → All2 Q l l'
  X : (∀ (x : A) (y : B), In y l' → P x → Q x y) → #|l'| = #|l| → All2 Q l l'
  x0 : A
  ============================
  ∀ y : B, In y l' → P x0 → Q x0 y
Debug:
  
  A : Type
  B : Type
  P : A → Type
  Q : A → B → Type
  b : B
  l' : list B
  x : A
  l : list A
  p : P x
  H1 : All P l
  H2 : ∀ (x : A) (y : B), In y (b :: l') → P x → Q x y
  H : #|l| = #|l'|
  IHAll : ∀ l' : list B,
            (∀ (x : A) (y : B), In y l' → P x → Q x y)
            → #|l'| = #|l| → All2 Q l l'
  X : (∀ (x : A) (y : B), In y l' → P x → Q x y) → #|l'| = #|l| → All2 Q l l'
  x0 : A
  y : B
  ============================
  In y l' → P x0 → Q x0 y
Debug:
  
  A : Type
  B : Type
  P : A → Type
  Q : A → B → Type
  b : B
  l' : list B
  x : A
  l : list A
  p : P x
  H1 : All P l
  H2 : ∀ (x : A) (y : B), In y (b :: l') → P x → Q x y
  H : #|l| = #|l'|
  IHAll : ∀ l' : list B,
            (∀ (x : A) (y : B), In y l' → P x → Q x y)
            → #|l'| = #|l| → All2 Q l l'
  X : (∀ (x : A) (y : B), In y l' → P x → Q x y) → #|l'| = #|l| → All2 Q l l'
  x0 : A
  y : B
  H0 : In y l'
  ============================
  P x0 → Q x0 y
Debug:
  
  A : Type
  B : Type
  P : A → Type
  Q : A → B → Type
  b : B
  l' : list B
  x : A
  l : list A
  p : P x
  H1 : All P l
  H2 : ∀ (x : A) (y : B), In y (b :: l') → P x → Q x y
  H : #|l| = #|l'|
  IHAll : ∀ l' : list B,
            (∀ (x : A) (y : B), In y l' → P x → Q x y)
            → #|l'| = #|l| → All2 Q l l'
  X : (∀ (x : A) (y : B), In y l' → P x → Q x y) → #|l'| = #|l| → All2 Q l l'
  x0 : A
  y : B
  H0 : In y l'
  X0 : P x0
  ============================
  Q x0 y
Debug:
  
  A : Type
  B : Type
  P : A → Type
  Q : A → B → Type
  b : B
  l' : list B
  x : A
  l : list A
  p : P x
  H1 : All P l
  H2 : ∀ (x : A) (y : B), In y (b :: l') → P x → Q x y
  H : #|l| = #|l'|
  IHAll : ∀ l' : list B,
            (∀ (x : A) (y : B), In y l' → P x → Q x y)
            → #|l'| = #|l| → All2 Q l l'
  X : (∀ (x : A) (y : B), In y l' → P x → Q x y) → #|l'| = #|l| → All2 Q l l'
  x0 : A
  y : B
  H0 : In y l'
  X0 : P x0
  X1 : ∀ y : B, In y (b :: l') → P x0 → Q x0 y
  ============================
  Q x0 y
Debug:
  
  A : Type
  B : Type
  P : A → Type
  Q : A → B → Type
  b : B
  l' : list B
  x : A
  l : list A
  p : P x
  H1 : All P l
  H2 : ∀ (x : A) (y : B), In y (b :: l') → P x → Q x y
  H : #|l| = #|l'|
  IHAll : ∀ l' : list B,
            (∀ (x : A) (y : B), In y l' → P x → Q x y)
            → #|l'| = #|l| → All2 Q l l'
  X : (∀ (x : A) (y : B), In y l' → P x → Q x y) → #|l'| = #|l| → All2 Q l l'
  x0 : A
  y : B
  H0 : In y l'
  X0 : P x0
  X1 : ∀ y : B, In y (b :: l') → P x0 → Q x0 y
  ============================
  Q x0 y
Debug:
  
  A : Type
  B : Type
  P : A → Type
  Q : A → B → Type
  b : B
  l' : list B
  x : A
  l : list A
  p : P x
  H1 : All P l
  H2 : ∀ (x : A) (y : B), In y (b :: l') → P x → Q x y
  H : #|l| = #|l'|
  IHAll : ∀ l' : list B,
            (∀ (x : A) (y : B), In y l' → P x → Q x y)
            → #|l'| = #|l| → All2 Q l l'
  X : (∀ (x : A) (y : B), In y l' → P x → Q x y) → #|l'| = #|l| → All2 Q l l'
  x0 : A
  y : B
  H0 : In y l'
  X0 : P x0
  X1 : ∀ y : B, In y (b :: l') → P x → Q x y
  ============================
  Q x0 y
Debug:
  
  A : Type
  B : Type
  P : A → Type
  Q : A → B → Type
  b : B
  l' : list B
  x : A
  l : list A
  p : P x
  H1 : All P l
  H2 : ∀ (x : A) (y : B), In y (b :: l') → P x → Q x y
  H : #|l| = #|l'|
  IHAll : ∀ l' : list B,
            (∀ (x : A) (y : B), In y l' → P x → Q x y)
            → #|l'| = #|l| → All2 Q l l'
  X : (∀ (x : A) (y : B), In y l' → P x → Q x y) → #|l'| = #|l| → All2 Q l l'
  x0 : A
  y : B
  H0 : In y l'
  X0 : P x0
  X1 : ∀ y : B, In y (b :: l') → P x → Q x y
  ============================
  Q x0 y
Debug:
  
  A : Type
  B : Type
  P : A → Type
  Q : A → B → Type
  b : B
  l' : list B
  x : A
  l : list A
  p : P x
  H1 : All P l
  H2 : ∀ (x : A) (y : B), In y (b :: l') → P x → Q x y
  H : #|l| = #|l'|
  IHAll : ∀ l' : list B,
            (∀ (x : A) (y : B), In y l' → P x → Q x y)
            → #|l'| = #|l| → All2 Q l l'
  X : (∀ (x : A) (y : B), In y l' → P x → Q x y) → #|l'| = #|l| → All2 Q l l'
  x0 : A
  y : B
  H0 : In y l'
  X0 : P x0
  ============================
  Q x0 y
Debug:
  
  A : Type
  B : Type
  P : A → Type
  Q : A → B → Type
  b : B
  l' : list B
  x : A
  l : list A
  p : P x
  H1 : All P l
  H2 : ∀ (x : A) (y : B), In y (b :: l') → P x → Q x y
  H : #|l| = #|l'|
  IHAll : ∀ l' : list B,
            (∀ (x : A) (y : B), In y l' → P x → Q x y)
            → #|l'| = #|l| → All2 Q l l'
  X : (∀ (x : A) (y : B), In y l' → P x → Q x y) → #|l'| = #|l| → All2 Q l l'
  ============================
  All2 Q l l'
Debug:
  
  A : Type
  B : Type
  P : A → Type
  Q : A → B → Type
  b : B
  l' : list B
  x : A
  l : list A
  p : P x
  H1 : All P l
  H2 : ∀ (x : A) (y : B), In y (b :: l') → P x → Q x y
  H : #|l| = #|l'|
  IHAll : ∀ l' : list B,
            (∀ (x : A) (y : B), In y l' → P x → Q x y)
            → #|l'| = #|l| → All2 Q l l'
  X : (∀ (x : A) (y : B), In y l' → P x → Q x y) → #|l'| = #|l| → All2 Q l l'
  X0 : ∀ y : B, In y (b :: l') → P x → Q x y
  ============================
  All2 Q l l'
Debug:
  
  A : Type
  B : Type
  P : A → Type
  Q : A → B → Type
  b : B
  l' : list B
  x : A
  l : list A
  p : P x
  H1 : All P l
  H2 : ∀ (x : A) (y : B), In y (b :: l') → P x → Q x y
  H : #|l| = #|l'|
  IHAll : ∀ l' : list B,
            (∀ (x : A) (y : B), In y l' → P x → Q x y)
            → #|l'| = #|l| → All2 Q l l'
  X0 : ∀ y : B, In y (b :: l') → P x → Q x y
  X : #|l'| = #|l| → All2 Q l l'
  ============================
  All2 Q l l'
Debug:
  
  A : Type
  B : Type
  P : A → Type
  Q : A → B → Type
  b : B
  l' : list B
  x : A
  l : list A
  p : P x
  H1 : All P l
  H2 : ∀ (x : A) (y : B), In y (b :: l') → P x → Q x y
  H : #|l| = #|l'|
  IHAll : ∀ l' : list B,
            (∀ (x : A) (y : B), In y l' → P x → Q x y)
            → #|l'| = #|l| → All2 Q l l'
  X0 : ∀ y : B, In y (b :: l') → P x → Q x y
  X : #|l'| = #|l| → All2 Q l l'
  ============================
  All2 Q l l'
Debug:
  
  A : Type
  B : Type
  P : A → Type
  Q : A → B → Type
  b : B
  l' : list B
  x : A
  l : list A
  p : P x
  H1 : All P l
  H2 : ∀ (x : A) (y : B), In y (b :: l') → P x → Q x y
  H : #|l| = #|l'|
  IHAll : ∀ l' : list B,
            (∀ (x : A) (y : B), In y l' → P x → Q x y)
            → #|l'| = #|l| → All2 Q l l'
  X0 : ∀ y : B, In y (b :: l') → P x → Q x y
  X : #|l'| = #|l| → All2 Q l l'
  ============================
  All2 Q l l'
Debug:
  
  A : Type
  B : Type
  P : A → Type
  Q : A → B → Type
  b : B
  l' : list B
  x : A
  l : list A
  p : P x
  H1 : All P l
  H2 : ∀ (x : A) (y : B), In y (b :: l') → P x → Q x y
  H : #|l| = #|l'|
  IHAll : ∀ l' : list B,
            (∀ (x : A) (y : B), In y l' → P x → Q x y)
            → #|l'| = #|l| → All2 Q l l'
  X : (∀ (x : A) (y : B), In y l' → P x → Q x y) → #|l'| = #|l| → All2 Q l l'
  X0 : ∀ y : B, In y (b :: l') → P x → Q x y
  ============================
  ∀ (x0 : A) (y : B), In y l' → P x0 → Q x0 y
Debug:
  
  A : Type
  B : Type
  P : A → Type
  Q : A → B → Type
  b : B
  l' : list B
  x : A
  l : list A
  p : P x
  H1 : All P l
  H2 : ∀ (x : A) (y : B), In y (b :: l') → P x → Q x y
  H : #|l| = #|l'|
  IHAll : ∀ l' : list B,
            (∀ (x : A) (y : B), In y l' → P x → Q x y)
            → #|l'| = #|l| → All2 Q l l'
  X : (∀ (x : A) (y : B), In y l' → P x → Q x y) → #|l'| = #|l| → All2 Q l l'
  X0 : ∀ y : B, In y (b :: l') → P x → Q x y
  x0 : A
  ============================
  ∀ y : B, In y l' → P x0 → Q x0 y
Debug:
  
  A : Type
  B : Type
  P : A → Type
  Q : A → B → Type
  b : B
  l' : list B
  x : A
  l : list A
  p : P x
  H1 : All P l
  H2 : ∀ (x : A) (y : B), In y (b :: l') → P x → Q x y
  H : #|l| = #|l'|
  IHAll : ∀ l' : list B,
            (∀ (x : A) (y : B), In y l' → P x → Q x y)
            → #|l'| = #|l| → All2 Q l l'
  X : (∀ (x : A) (y : B), In y l' → P x → Q x y) → #|l'| = #|l| → All2 Q l l'
  X0 : ∀ y : B, In y (b :: l') → P x → Q x y
  x0 : A
  y : B
  ============================
  In y l' → P x0 → Q x0 y
Debug:
  
  A : Type
  B : Type
  P : A → Type
  Q : A → B → Type
  b : B
  l' : list B
  x : A
  l : list A
  p : P x
  H1 : All P l
  H2 : ∀ (x : A) (y : B), In y (b :: l') → P x → Q x y
  H : #|l| = #|l'|
  IHAll : ∀ l' : list B,
            (∀ (x : A) (y : B), In y l' → P x → Q x y)
            → #|l'| = #|l| → All2 Q l l'
  X : (∀ (x : A) (y : B), In y l' → P x → Q x y) → #|l'| = #|l| → All2 Q l l'
  X0 : ∀ y : B, In y (b :: l') → P x → Q x y
  x0 : A
  y : B
  H0 : In y l'
  ============================
  P x0 → Q x0 y
Debug:
  
  A : Type
  B : Type
  P : A → Type
  Q : A → B → Type
  b : B
  l' : list B
  x : A
  l : list A
  p : P x
  H1 : All P l
  H2 : ∀ (x : A) (y : B), In y (b :: l') → P x → Q x y
  H : #|l| = #|l'|
  IHAll : ∀ l' : list B,
            (∀ (x : A) (y : B), In y l' → P x → Q x y)
            → #|l'| = #|l| → All2 Q l l'
  X : (∀ (x : A) (y : B), In y l' → P x → Q x y) → #|l'| = #|l| → All2 Q l l'
  X0 : ∀ y : B, In y (b :: l') → P x → Q x y
  x0 : A
  y : B
  H0 : In y l'
  X1 : P x0
  ============================
  Q x0 y
Debug:
  
  A : Type
  B : Type
  P : A → Type
  Q : A → B → Type
  b : B
  l' : list B
  x : A
  l : list A
  p : P x
  H1 : All P l
  H2 : ∀ (x : A) (y : B), In y (b :: l') → P x → Q x y
  H : #|l| = #|l'|
  IHAll : ∀ l' : list B,
            (∀ (x : A) (y : B), In y l' → P x → Q x y)
            → #|l'| = #|l| → All2 Q l l'
  X : (∀ (x : A) (y : B), In y l' → P x → Q x y) → #|l'| = #|l| → All2 Q l l'
  X0 : ∀ y : B, In y (b :: l') → P x → Q x y
  x0 : A
  y : B
  H0 : In y l'
  X1 : P x0
  ============================
  Q x0 y
Debug:
  
  A : Type
  B : Type
  P : A → Type
  Q : A → B → Type
  b : B
  l' : list B
  x : A
  l : list A
  p : P x
  H1 : All P l
  H2 : ∀ (x : A) (y : B), In y (b :: l') → P x → Q x y
  H : #|l| = #|l'|
  IHAll : ∀ l' : list B,
            (∀ (x : A) (y : B), In y l' → P x → Q x y)
            → #|l'| = #|l| → All2 Q l l'
  X : (∀ (x : A) (y : B), In y l' → P x → Q x y) → #|l'| = #|l| → All2 Q l l'
  X0 : ∀ y : B, In y (b :: l') → P x → Q x y
  ============================
  All2 Q l l'
Debug:
  
  A : Type
  B : Type
  P : A → Type
  Q : A → B → Type
  b : B
  l' : list B
  x : A
  l : list A
  p : P x
  H1 : All P l
  H2 : ∀ (x : A) (y : B), In y (b :: l') → P x → Q x y
  H : #|l| = #|l'|
  IHAll : ∀ l' : list B,
            (∀ (x : A) (y : B), In y l' → P x → Q x y)
            → #|l'| = #|l| → All2 Q l l'
  X : (∀ (x : A) (y : B), In y l' → P x → Q x y) → #|l'| = #|l| → All2 Q l l'
  X0 : ∀ y : B, In y (b :: l') → P x → Q x y
  X1 : B
  X2 : In X1 (b :: l') → P x → Q x X1
  ============================
  All2 Q l l'
Debug:
  
  A : Type
  B : Type
  P : A → Type
  Q : A → B → Type
  b : B
  l' : list B
  x : A
  l : list A
  p : P x
  H1 : All P l
  H2 : ∀ (x : A) (y : B), In y (b :: l') → P x → Q x y
  H : #|l| = #|l'|
  IHAll : ∀ l' : list B,
            (∀ (x : A) (y : B), In y l' → P x → Q x y)
            → #|l'| = #|l| → All2 Q l l'
  X : (∀ (x : A) (y : B), In y l' → P x → Q x y) → #|l'| = #|l| → All2 Q l l'
  X0 : ∀ y : B, In y (b :: l') → P x → Q x y
  X1 : B
  X2 : b = X1 → P x → Q x X1
  X3 : (fix In (a : B) (l : list B) {struct l} : Prop :=
          match l with
          | [] => False
          | b :: m => b = a ∨ In a m
          end) X1 l' → P x → Q x X1
  ============================
  All2 Q l l'
Debug:
  
  A : Type
  B : Type
  P : A → Type
  Q : A → B → Type
  b : B
  l' : list B
  x : A
  l : list A
  p : P x
  H1 : All P l
  H2 : ∀ (x : A) (y : B), In y (b :: l') → P x → Q x y
  H : #|l| = #|l'|
  IHAll : ∀ l' : list B,
            (∀ (x : A) (y : B), In y l' → P x → Q x y)
            → #|l'| = #|l| → All2 Q l l'
  X : (∀ (x : A) (y : B), In y l' → P x → Q x y) → #|l'| = #|l| → All2 Q l l'
  X0 : ∀ y : B, In y (b :: l') → P x → Q x y
  X1 : B
  X2 : b = X1 → P x → Q x X1
  X3 : (fix In (a : B) (l : list B) {struct l} : Prop :=
          match l with
          | [] => False
          | b :: m => b = a ∨ In a m
          end) X1 l' → P x → Q x X1
  ============================
  All2 Q l l'
Debug:
  
  A : Type
  B : Type
  P : A → Type
  Q : A → B → Type
  b : B
  l' : list B
  x : A
  l : list A
  p : P x
  H1 : All P l
  H2 : ∀ (x : A) (y : B), In y (b :: l') → P x → Q x y
  H : #|l| = #|l'|
  IHAll : ∀ l' : list B,
            (∀ (x : A) (y : B), In y l' → P x → Q x y)
            → #|l'| = #|l| → All2 Q l l'
  X : (∀ (x : A) (y : B), In y l' → P x → Q x y) → #|l'| = #|l| → All2 Q l l'
  X0 : ∀ y : B, In y (b :: l') → P x → Q x y
  X1 : B
  X2 : b = X1 → P x → Q x X1
  X3 : (fix In (a : B) (l : list B) {struct l} : Prop :=
          match l with
          | [] => False
          | b :: m => b = a ∨ In a m
          end) X1 l' → P x → Q x X1
  ============================
  All2 Q l l'
Debug:
  
  A : Type
  B : Type
  P : A → Type
  Q : A → B → Type
  b : B
  l' : list B
  x : A
  l : list A
  p : P x
  H1 : All P l
  H2 : ∀ (x : A) (y : B), In y (b :: l') → P x → Q x y
  H : #|l| = #|l'|
  IHAll : ∀ l' : list B,
            (∀ (x : A) (y : B), In y l' → P x → Q x y)
            → #|l'| = #|l| → All2 Q l l'
  X : (∀ (x : A) (y : B), In y l' → P x → Q x y) → #|l'| = #|l| → All2 Q l l'
  X0 : ∀ y : B, In y (b :: l') → P x → Q x y
  X1 : B
  X2 : b = X1 → P x → Q x X1
  X3 : (fix In (a : B) (l : list B) {struct l} : Prop :=
          match l with
          | [] => False
          | b :: m => b = a ∨ In a m
          end) X1 l' → P x → Q x X1
  ============================
  All2 Q l l'
Debug:
  
  A : Type
  B : Type
  P : A → Type
  Q : A → B → Type
  b : B
  l' : list B
  x : A
  l : list A
  p : P x
  H1 : All P l
  H2 : ∀ (x : A) (y : B), In y (b :: l') → P x → Q x y
  H : #|l| = #|l'|
  IHAll : ∀ l' : list B,
            (∀ (x : A) (y : B), In y l' → P x → Q x y)
            → #|l'| = #|l| → All2 Q l l'
  X : (∀ (x : A) (y : B), In y l' → P x → Q x y) → #|l'| = #|l| → All2 Q l l'
  X0 : ∀ y : B, In y (b :: l') → P x → Q x y
  X1 : B
  X2 : b = X1 → P x → Q x X1
  X3 : (fix In (a : B) (l : list B) {struct l} : Prop :=
          match l with
          | [] => False
          | b :: m => b = a ∨ In a m
          end) X1 l' → P x → Q x X1
  ============================
  All2 Q l l'
Debug:
  
  A : Type
  B : Type
  P : A → Type
  Q : A → B → Type
  b : B
  l' : list B
  x : A
  l : list A
  p : P x
  H1 : All P l
  H2 : ∀ (x : A) (y : B), In y (b :: l') → P x → Q x y
  H : #|l| = #|l'|
  IHAll : ∀ l' : list B,
            (∀ (x : A) (y : B), In y l' → P x → Q x y)
            → #|l'| = #|l| → All2 Q l l'
  X : (∀ (x : A) (y : B), In y l' → P x → Q x y) → #|l'| = #|l| → All2 Q l l'
  X0 : ∀ y : B, In y (b :: l') → P x → Q x y
  ============================
  All2 Q l l'
Debug:
  
  A : Type
  B : Type
  P : A → Type
  Q : A → B → Type
  b : B
  l' : list B
  x : A
  l : list A
  p : P x
  H1 : All P l
  H2 : ∀ (x : A) (y : B), In y (b :: l') → P x → Q x y
  H : #|l| = #|l'|
  IHAll : ∀ l' : list B,
            (∀ (x : A) (y : B), In y l' → P x → Q x y)
            → #|l'| = #|l| → All2 Q l l'
  X : (∀ (x : A) (y : B), In y l' → P x → Q x y) → #|l'| = #|l| → All2 Q l l'
  ============================
  All2 Q l l'
Debug:
  
  A : Type
  B : Type
  P : A → Type
  Q : A → B → Type
  b : B
  l' : list B
  x : A
  l : list A
  p : P x
  H1 : All P l
  H2 : ∀ (x : A) (y : B), In y (b :: l') → P x → Q x y
  H : #|l| = #|l'|
  IHAll : ∀ l' : list B,
            (∀ (x : A) (y : B), In y l' → P x → Q x y)
            → #|l'| = #|l| → All2 Q l l'
  ============================
  All2 Q l l'