title: Is there any non-trivial code that uses Data.Maybe.Is-just?
body: <p>The Agda standard library provides a data type <code>Maybe</code> accompanied with a view <code>Any</code>.
  Then there is the property <code>Is-just</code> defined using <code>Any</code>. I found working with this type difficult as the standard library provides exactly no tooling for <code>Any</code>.</p>
  
  <p>Thus I am looking for examples on how to work with <code>Is-just</code> effectively. Is there an open source project that uses it?</p>
  
  <p>Alternatively, I am seeking how to put it to good use:</p>
  
  <ul>
  <li>Given <code>Is-just m</code> and <code>Is-nothing m</code>, how to eliminate? Can <code>Relation.Nullary.Negation.contradiction</code> be used here?</li>
  <li>Given a property <code>p : ... → (mp : Is-just m) → ... → ... ≡ to-witness mp</code> that needs to be shown inductively by <code>p ... = {! p ... (subst Is-just m≡somethingelse mp) ... !}</code>, the given term does not fill the hole, because it has type <code>... ≡ to-witness (subst Is-just m≡somethingelse mp)</code>.</li>
  </ul>
  
  <p>Often it seems easier to work with <code>Σ A (_≡_ m ∘ just)</code> than <code>Is-just m</code>.</p>