Eu venho de um background de programação JavaScript / Ruby e estou acostumado a isso como true / false funciona (em JS):

!true
// false
!false
// true

Então você pode usar esses valores verdadeiro / falso com&& gostar

var a = true, b = false;
a && !b;

assime enão (e outros operadores lógicos / booleanos) fazem parte de um único sistema; parece que o sistema "lógico" e o sistema "booleano" são o mesmo.

No entanto, no Coq, lógicas e booleanos são duas coisas separadas. Por que é isso? A citação / link abaixo demonstra como um teorema é necessário para relacioná-los.

Já vimos vários lugares onde estruturas análogas podem ser encontradas nos mundos computacional (Tipo) e lógico (Prop) da Coq. Aqui está mais um: os operadores booleanos andb e orb são claramente análogos dos conectivos lógicos ∧ e ∨. Essa analogia pode ser mais precisa com os seguintes teoremas, que mostram como traduzir o conhecimento sobre os comportamentos de andb e orb em certas entradas em fatos proposicionais sobre essas entradas.

Theorem andb_prop : ∀b c,
  andb b c = true → b = true ∧ c = true.

http://www.seas.upenn.edu/~cis500/current/sf/Logic.html#lab211