title: Agda: proving that, when values are equal, their constructor arguments are equal
body: <p>I'm trying to write the following function:</p>
  
  <pre><code>justEq : ∀ {A} -&gt; (x y : A) -&gt; (just x ≡ just y) -&gt; (x ≡ y)
  justEq x y pf = {!!}
  </code></pre>
  
  <p>I don't know how to write this. To me, it is intuitive to the point of being axiomatic, but the compiler doesn't accept refl as a proof of it.</p>
  
  <p>I'm routinely having to prove these sorts of things, for example, showing that if two non-empty lists are equal, then their heads are equal.</p>
  
  <p>What is the general approach to this? Is this related to Conor McBride's "green-goo" of having functions in the return of Constructors?</p>