title: Is it possible to import a file in a proof only in Coq?
body: <p>I'm looking for something like this</p>
  <p>Suppose I have a lemma that is using some long named module</p>
  <pre><code>Lemma foo : SomeLongNamedModule.foo = blablabla.
  
  </code></pre>
  <p>I want to import <code>SomeLongNamedModule</code> inside the proof but left scope outside of the proof clean. I'm looking for something like this</p>
  <pre><code>Lemma foo : SomeLongNamedModule.foo = blablabla
    Local Import SomeLongNamedModule
    ...
  
  Qed
  
  (* Here SomeLongNamedModule is not polluting the scope *)
  </code></pre>
  <p>Is that possible? I think about wrapping it in a module but it seems overkill to me. To explain my use case, I'm working on a code base where we avoid <code>Import</code>, but during the
  writing of proofs I insert the <code>Import</code> and then remove it later and refactor the proof.
  If there is something <code>Local Import</code> it would be possible left it there in some cases.</p>
  <p>One option is using modules, this works</p>
  <pre><code>Module Bar.
    Parameter bar : forall {A : Type}, A -&gt; A.
  End Bar.
  
  Module Foo.
    Import Bar.
  
    Check bar.
  End Foo.
  
  Fail Check bar. (* bar not defined here *)
  </code></pre>
  <p>My guess is that Lemma is not a scope so I can't do this.</p>