<html>
  <head>

    <meta http-equiv="content-type" content="text/html; charset=UTF-8">
  </head>
  <body text="#000000" bgcolor="#FFFFFF">
    Assuming a predicate <i>even</i><br>
    <p><b>data even :  ℕ -> Set where</b><b><br>
      </b><b>  even0 : even zero</b><b><br>
      </b><b>  even1 : even (suc zero)</b><b><br>
      </b><b>  evenSS : {n : ℕ} -> even n -> even (suc (suc n))</b></p>
    <p>I would like to prove:</p>
    <p><b>inversionEven : {n : ℕ} -> even (suc (suc n)) -> even n</b></p>
    <p>In Coq, I could use <br>
    </p>
    <ul>
      <li>either a command <i>inversion</i></li>
      <li>or a somewhat direct proof<i> </i>that applies even_ind. </li>
    </ul>
    <p>Are there similar features in Agda ?<br>
    </p>
    <pre class="moz-signature" cols="72">-- 
Cheers

---------------------------
Pierre Lescanne (Emeritus Professor)
LIP / École normale supérieure de Lyon
46 allée d'Italie
69364 LYON Cedex 07, France
tél: +33 6 85 70 94 31
<a class="moz-txt-link-freetext" href="http://perso.ens-lyon.fr/pierre.lescanne/">http://perso.ens-lyon.fr/pierre.lescanne/</a>
---------------------------
</pre>
  </body>
</html>