Definition listInduction8 :
  forall (A : Type),
  forall (P : list A -> Prop),
  P [] ->
  (forall (b0                      : A), P (b0 :: [])) ->
  (forall (b1 b0                   : A), P (b1 :: b0 :: [])) ->
  (forall (b2 b1 b0                : A), P (b2 :: b1 :: b0 :: [])) ->
  (forall (b3 b2 b1 b0             : A), P (b3 :: b2 :: b1 :: b0 :: [])) ->
  (forall (b4 b3 b2 b1 b0          : A), P (b4 :: b3 :: b2 :: b1 :: b0 :: [])) ->
  (forall (b5 b4 b3 b2 b1 b0       : A), P (b5 :: b4 :: b3 :: b2 :: b1 :: b0 :: [])) ->
  (forall (b6 b5 b4 b3 b2 b1 b0    : A), P (b6 :: b5 :: b4 :: b3 :: b2 :: b1 :: b0 :: [])) ->
  (forall (b7 b6 b5 b4 b3 b2 b1 b0 : A) (rest : list A), P rest -> P (b7 :: b6 :: b5 :: b4 :: b3 :: b2 :: b1 :: b0 :: rest)) ->
  forall (L : list A), P L :=
  (fun A P P0 P1 P2 P3 P4 P5 P6 P7 P8 =>
  fix f (l : list A) :=
    match l with
    | []                                                     => P0
    | x0 :: []                                               => P1 x0
    | (x0 :: x1 :: [])                                       => P2 x0 x1
    | (x0 :: x1 :: x2 :: [])                                 => P3 x0 x1 x2
    | (x0 :: x1 :: x2 :: x3 :: [])                           => P4 x0 x1 x2 x3
    | (x0 :: x1 :: x2 :: x3 :: x4 :: [])                     => P5 x0 x1 x2 x3 x4
    | (x0 :: x1 :: x2 :: x3 :: x4 :: x5 :: [])               => P6 x0 x1 x2 x3 x4 x5
    | (x0 :: x1 :: x2 :: x3 :: x4 :: x5 :: x6 :: [])         => P7 x0 x1 x2 x3 x4 x5 x6
    | (x0 :: x1 :: x2 :: x3 :: x4 :: x5 :: x6 :: x7 :: rest) => P8 x0 x1 x2 x3 x4 x5 x6 x7 rest (f rest)
    end).
