title: Type inference to unification problem
body: <p>Has anyone an idea how the type inference problem </p>
  
  <pre><code>E &gt; hd (cons 1 nil) : α0
  </code></pre>
  
  <p>with the typing environment</p>
  
  <pre><code>                E={
                     hd : list(α1 ) → α1 ,
                     cons : α2 → list(α2 ) → list(α2 ),
                     nil : list(α3 ),
                     1 : int
                  }
  </code></pre>
  
  <p>can be transferred in an unification problem?</p>
  
  <p>Any help would really be appreciated!</p>