<div dir="ltr"><div><div><div>Maybe you can explain what approaches you have already tried and why you got stuck? I think people would be more inclined to help that way.<br><br></div>To get you started on proof1, here's a hint: since you are proving something about the functions foldr₁ and _⊔_, you can take a look at their definitions and follow the same structure for your proof. For example, since foldr₁ is defined in terms of the helper function foldr, you probably also need to define a helper lemma that proves a similar statement about foldr.<br><br></div>Best regards,<br></div>Jesper<br></div><div class="gmail_extra"><br><div class="gmail_quote">2017-08-14 18:33 GMT+02:00 Serge Leblanc <span dir="ltr"><<a href="mailto:33dbqnxpy7if@gmail.com" target="_blank">33dbqnxpy7if@gmail.com</a>></span>:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
  
    
  
  <div text="#000000" bgcolor="#FFFFFF">
    <p>Saluton, neniu bonvolas helpi min?<br>
    </p>
    <p>Hi, nobody wants to help me?<br>
    </p><div><div class="h5">
    <br>
    <div class="m_-5308586550852440085moz-cite-prefix">On 2017-08-06 18:23, Serge Leblanc
      wrote:<br>
    </div>
    <blockquote type="cite">
      
      <span id="m_-5308586550852440085result_box" lang="en"><span>Dear All,</span><br>
        <span>I need help to finish these lemmas.</span><br>
        <span>They have the same meaning, I am right?</span><br>
        <span>All helpers are welcome!</span></span><br>
      <br>
      Estimata ĉiuj, <br>
      Mi bezonas helpon por daŭrigi ci-tiuj pruvojn!<br>
      <div class="m_-5308586550852440085moz-signature">Ĉu ili havas je la saman signifon! Ĉu
        mi pravas?<br>
        Ĉiuj helpantoj estas bonvenaj!<br>
        <br>
        Sincere.<br>
        -- <br>
        Serge Leblanc
        <hr> gpg --search-keys 0x67B17A3F <br>
        Fingerprint = 2B2D AC93 8620 43D3 D2C2 C2D3 B67C F631 67B1 7A3F</div>
    </blockquote>
    <br>
    <div class="m_-5308586550852440085moz-signature">-- <br>
      Serge Leblanc
      <hr>
      gpg --search-keys 0x67B17A3F
      <br>
      Fingerprint = 2B2D AC93 8620 43D3 D2C2 C2D3 B67C F631 67B1 7A3F</div>
  </div></div></div>

<br>______________________________<wbr>_________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/<wbr>mailman/listinfo/agda</a><br>
<br></blockquote></div><br></div>