<html>
  <head>

    <meta http-equiv="content-type" content="text/html; charset=UTF-8">
  </head>
  <body>
    I have a problem with the two lines below in the context <br>
    open import Data.Product using (_×_; proj₁; proj₂) renaming (_,_ to
    ⟨_,_⟩)<br>
    <p>test0 : 1 ≡ proj₁ ⟨ 1 , 2 ⟩<br>
      test0 = refl</p>
    <p>———— Errors ————————————————————————————————————————————————<br>
      Failed to solve the following constraints:<br>
        _50 := 2 [blocked on problem 99]<br>
        [99] ℕ =< _B_49 1 : Set</p>
    <p>The term proj₁ ⟨ 1 , 2 ⟩ appears in <u>yellow</u> and its value
      calculated by C-c C-n is 1</p>
    <p><br>
    </p>
    <p>Still more strange, when I rename proj₁ in proj1 with <br>
    </p>
    <p>proj1 : {A B : Set} -> A × B -> A<br>
      proj1 ⟨ x , y ⟩ = x<br>
    </p>
    <p>I have without error</p>
    <p>test0' : 1 ≡ proj1 ⟨ 1 , 2 ⟩<br>
      test0' = refl<br>
    </p>
    <div class="moz-signature">-- <br>
      courriel : <a class="moz-txt-link-abbreviated" href="mailto:michel.levy.imag@free.fr">michel.levy.imag@free.fr</a> <br>
      mobile : 06 59 13 42 53<br>
      web : michel.levy.imag.free.fr
    </div>
  </body>
</html>