title: Proof irrelevance (2)
body: <p>Let's assume we have two proofs for a simple lemma.</p>
  
  <pre><code>   Lemma l1: exists x:nat, x &lt;&gt; 0.
      exists 1.
      intro.
      discriminate.
      Defined.
  
      Lemma l2: exists x:nat, x &lt;&gt; 0.
      exists 2.
      discriminate.
      Defined.
  </code></pre>
  
  <p>Intuitively, I would say that those are two different proofs.
  So, can I prove the following lemma?</p>
  
  <pre><code>Lemma l3: l1 &lt;&gt; l2 
  </code></pre>
  
  <p>I suppose this is undecidable.<br>
  What happens if we introduce the Univalence Axiom ?</p>