✓

@Book{            book:965499,
  Author        = "Bertot, Yves and Cast{\'e}ran, Pierre",
  date-added    = "2020-04-10 11:07:26 +0200",
  date-modified = "2020-04-10 11:07:26 +0200",
  ISBN          = "978-3-642-05880-6,978-3-662-07964-5",
  Publisher     = "Springer",
  Series        = "Texts in Theoretical Computer Science An EATCS Series",
  Title         = "Interactive Theorem Proving and Program Development: Coq'Art: The Calculus of Inductive Constructions",
  URL           = "http://gen.lib.rus.ec/book/index.php?md5=af031a5eb2d351217f52eefd8c1555ac",
  Year          = "2004",
  bdsk-url-1    = "http://gen.lib.rus.ec/book/index.php?md5=af031a5eb2d351217f52eefd8c1555ac",
  File          = "Interactive\_Theorem\_Proving\_Coq (0) - a - a.pdf"
}

@Book{ book:965499, Author = "Bertot, Yves and Cast{\'e}ran, Pierre", date-added = "2020-04-10 11:07:26 +0200", date-modified = "2020-04-10 11:07:26 +0200", ISBN = "978-3-642-05880-6,978-3-662-07964-5", Publisher = "Springer", Series = "Texts in Theoretical Computer Science An EATCS Series", Title = "Interactive Theorem Proving and Program Development: Coq'Art: The Calculus of Inductive Constructions", URL = "http://gen.lib.rus.ec/book/index.php?md5=af031a5eb2d351217f52eefd8c1555ac", Year = "2004", bdsk-url-1 = "http://gen.lib.rus.ec/book/index.php?md5=af031a5eb2d351217f52eefd8c1555ac", File = "Interactive_Theorem_Proving_Coq (0) - a - a.pdf" }