title: Does ssreflect assume excluded middle?
body: <p>I am reading the ssreflect tutorial, <a href="https://hal.inria.fr/inria-00407778/file/RT-367.pdf" rel="noreferrer">which reads</a>:</p>
  
  <blockquote>
    <p>Below, we prove the ... by translating the propositional statement
    into its boolean counterpart, which is easily proved using brute
    force. This proof technique is called reflection. Ssreflect’s design
    allows for and ssreflect’s spirit recommends wide use of such a
    technique.</p>
  </blockquote>
  
  <p>Does this (reflection) mean that the ssreflect assumes the excluded middle (<code>forall A:Prop, A \/ ~A</code>)?</p>
  
  <p>It looks that it's the case because all boolean values satisfy the E.M. If so, this would be a big assumption to make for following the ssreflect style. </p>
  
  <p>Also, I don't quite understand the "local" or "small scale" part of it that follows:</p>
  
  <blockquote>
    <p>Since it is usually used locally to handle efficiently small parts of
    the proofs (instead of being used in the overall proof structure),
    this is called small scale reflection, hence the name ssreflect.</p>
  </blockquote>
  
  <p>What does it mean small parts v.s. the overall proof structure. Is this implying that we can assume E.M. locally sometimes with no harm and do not use E.M. in general, or does the local here mean something else?</p>
  
  <p>Also, I am not experienced enough in Coq, and don't quite see how this "brute force" style on the "boolean counterparts" (mostly based on <code>case</code> analysis from what I read so far) is more efficient than the vanilla Coq way. To me, brute force is not very intuitive and not easy to guess beforehand until you see the result. </p>
  
  <p>Any concrete examples to illustrate the efficiency here?</p>