<div dir="ltr">Hi,<div><br></div><div>currently agda won&#39;t accept code like this:</div><div><br></div><div><div>test0 : ∀ {F : ℕ -&gt; ℕ} -&gt; (\ x -&gt; suc (F x)) ≡ (\ x -&gt; suc (suc x)) -&gt; ℕ</div><div>test0 {.suc} refl = ?</div>
</div><div><br></div><div>reporting that &quot;F x&quot; is not the same as &quot;suc x&quot;.</div><div><br></div><div>Interestingly we can actually derive &quot;F  ≡ suc&quot; through &quot;cong (\ f x -&gt; pred (f x)) p&quot;, and in general instead of pred we can use a function like strip</div>
<div><br></div><div>strip x (con y) = y</div><div>strip x _ = G x</div><div><br></div><div>to handle equations like (\x -&gt; con (F x)) ≡ (\x -&gt; con (G x)).</div><div><br></div><div>Such equations come up all the time when trying to do induction on representations in the style of &quot;Outrageous but Meaningful Coincidences&quot;[1], so it&#39;d be nice to have native support.</div>
<div><br></div><div>It would actually be great to be able to recognize as empty things like </div><div>(\ (x : A) -&gt; true) ≡ (\ x -&gt; false), but that seems refutable only when you have an element of A.</div><div><br>
</div><div> </div><div>Cheers,</div><div>Andrea</div><div><br></div><div>[1]<a href="http://dl.acm.org/citation.cfm?id=1863497">http://dl.acm.org/citation.cfm?id=1863497</a></div><div><br></div><div><br></div><div><br></div>
<div><br></div><div><br></div><div><br></div></div>