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 l l')


DEBUG:Going to execute:
eapply IHAll

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'
  ============================
   (∀ (x : A) (y : B), In y l' → P x → Q x y)

  
  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'
  ============================
   (#|l'| = #|l|)


DEBUG:Going to execute:
firstorder
DEBUG LTAC Evaluated term: IHAll

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'
  ============================
   (∀ (x : A) (y : B), In y l' → P x → Q x y)

  
  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'
  ============================
   (#|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'
  ============================
  ∀ (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'
  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'
  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'
  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'
  x0 : A
  y : B
  H0 : In y l'
  X : 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'
  x0 : A
  y : B
  H0 : In y l'
  X : P x0
  X0 : ∀ 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'
  x0 : A
  y : B
  H0 : In y l'
  X : P x0
  X0 : ∀ y : B, In y (b :: l') → P x0 → Q x0 y
  X1 : 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'
  x0 : A
  y : B
  H0 : In y l'
  X : P x0
  X0 : ∀ y : B, In y (b :: l') → P x0 → Q x0 y
  X1 : b = y → P x0 → Q x0 y
  X2 : (fix In (a : B) (l : list B) {struct l} : Prop :=
          match l with
          | [] => False
          | b :: m => b = a ∨ In a m
          end) y 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'
  x0 : A
  y : B
  H0 : In y l'
  X : P x0
  X0 : ∀ y : B, In y (b :: l') → P x0 → Q x0 y
  X1 : b = y → P x0 → Q x0 y
  X2 : (fix In (a : B) (l : list B) {struct l} : Prop :=
          match l with
          | [] => False
          | b :: m => b = a ∨ In a m
          end) y 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'
  x0 : A
  y : B
  H0 : In y l'
  X : P x0
  X0 : ∀ y : B, In y (b :: l') → P x0 → Q x0 y
  X1 : b = y → P x0 → Q x0 y
  X2 : 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'
  x0 : A
  y : B
  H0 : In y l'
  X : P x0
  X0 : ∀ y : B, In y (b :: l') → P x0 → Q x0 y
  X1 : b = y → P x0 → Q x0 y
  X2 : 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'
  x0 : A
  y : B
  H0 : In y l'
  X : P x0
  X0 : ∀ y : B, In y (b :: l') → P x0 → Q x0 y
  X1 : b = y → P x0 → Q x0 y
  X2 : 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'
  ============================
  #|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'
  ============================
  #|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
  ============================
  #|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
  ============================
  #|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'
  ============================
  #|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'
  ============================
  #|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'
  ============================
  #|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'
  ============================
  #|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'
  ============================
  #|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'
  ============================
  #|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'
  ============================
  #|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
  ============================
  #|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
  ============================
  #|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
  ============================
  #|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
  ============================
  #|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
  ============================
  #|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
  ============================
  #|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
  ============================
  #|l'| = #|l|