Goal:
  
  A : Type
  size : A → nat
  a : A
  l : list A
  l' : list A
  IHl : BinInt.Z.of_nat (list_size (l ++ l')) =
        BinInt.Z.add (BinInt.Z.of_nat (list_size l))
          (BinInt.Z.of_nat (list_size l'))
  cstr : BinInt.Z.le BinNums.Z0 (BinInt.Z.of_nat (size a))
  cstr0 : BinInt.Z.le BinNums.Z0 (BinInt.Z.of_nat (list_size l))
  cstr1 : BinInt.Z.le BinNums.Z0 (BinInt.Z.of_nat (list_size l'))
  cstr2 : BinInt.Z.le BinNums.Z0 (BinInt.Z.of_nat (list_size (l ++ l')))
  ============================
   (BinInt.Z.add
      (BinInt.Z.add (BinInt.Z.of_nat (size a))
         (BinInt.Z.add (BinInt.Z.of_nat (list_size l))
            (BinInt.Z.of_nat (list_size l')))) (BinNums.Zpos BinNums.xH) =
    BinInt.Z.add
      (BinInt.Z.add
         (BinInt.Z.add (BinInt.Z.of_nat (size a))
            (BinInt.Z.of_nat (list_size l))) (BinInt.Z.of_nat (list_size l')))
      (BinNums.Zpos BinNums.xH))


DEBUG:Going to execute:
idtac