<div dir="ltr"><div dir="ltr"><div>You can try this function : <br></div><div>```<br>failed : ∀ {Σ' Σ t} → t ∈ Σ → Σ' ⊑ₕ Σ → Type<br>failed {Σ'} mem prec with length Σ' | ⊑ₕ-length prec<br>failed {Σ'} mem prec | _ | refl = {!!}<br></div><div>```<br></div></div></div><br><div class="gmail_quote"><div dir="ltr">On Tue, Jan 8, 2019 at 5:48 AM Deyaaeldeen <<a href="mailto:diaa6510@gmail.com">diaa6510@gmail.com</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><div dir="ltr"><div dir="ltr"><div>Hello,</div><div><br></div><div>I want to use the fact that two lists have the same length if they are Pointwise, witnessed by the Pointwise-length function. However, Agda complains about the constructor refl at line 51 in the</div><div>self-contained agda file located here:</div><div><a href="https://gist.github.com/deyaaeldeen/1fbc17082f6af8c2d3e45849abacdd51" target="_blank">https://gist.github.com/deyaaeldeen/1fbc17082f6af8c2d3e45849abacdd51</a><br></div><div><br></div><div>Your input is much appreciated.</div><br clear="all"><div><div dir="rtl" class="gmail-m_-124825370402391504gmail_signature"><div dir="ltr"><div><div dir="rtl"><div style="text-align:left">Deyaa<br></div></div></div></div></div></div></div></div>
_______________________________________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
</blockquote></div>