Goal:
  
  A : Type
  size : A → nat
  a : A
  l : list A
  IHl : BinInt.Z.of_nat (list_size (rev 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 (rev l)))
  cstr1 : BinInt.Z.le BinNums.Z0 (BinInt.Z.of_nat (list_size l))
  ============================
   (BinInt.Z.add (BinInt.Z.of_nat (list_size l))
      (BinInt.Z.add (BinInt.Z.add (BinInt.Z.of_nat (size a)) BinNums.Z0)
         (BinNums.Zpos BinNums.xH)) =
    BinInt.Z.add
      (BinInt.Z.add (BinInt.Z.of_nat (size a))
         (BinInt.Z.of_nat (list_size l))) (BinNums.Zpos BinNums.xH))


DEBUG:Going to execute:
idtac