title: How to use Streicher_K_ Axiom
body: <p>can someone show me a simple example how to use the <code>Streicher_K_</code> axiom from <code>Coq.Logic.EqdepFacts</code>?</p>
  
  <p>Maybe for showing the simple fact:  </p>
  
  <pre><code>Lemma single_proof : forall (A:Type)(x y:A) (u v:x = y), u = v.
  </code></pre>
  
  <p>I managed to prove it with <code>Streicher_K_on_</code>:</p>
  
  <pre><code>Variable A:Type.
  Variable x:A. 
  Axiom SK:Streicher_K_on_ A x (fun p:x=x =&gt; (eq_refl x) = p).
  
  Lemma single_proof : forall (y:A)(u v:x = y), u = v.
  intros.
  destruct u.
  apply (SK).
  reflexivity.
  Qed. 
  </code></pre>
  
  <p>By trial and error I also found out how to prove it with <code>Streicher_K_</code> , which is even more simple: </p>
  
  <pre><code>Axiom SK:Streicher_K_ A. 
  </code></pre>
  
  <p>But the problem is that I have no idea why this works. I don't understand the underlying type checking.</p>