<div dir="ltr"><div>I'm in a situation where I'm using "agda --without k", and I'm working with a with decidable equality.</div><div><br></div><div>In my proofs, a bunch of normalizations are stuck on "decEq i i". I have a proof of the form "uipDec : \forall i -> decEq i i \equiv yes refl", but when I try to "rewrite uipDec", I get:</div><div><br></div><div>decEq i i != lhs of type Dec (i ≡ i)<br>when checking that the type decEq i i != lhs of type Dec (i ≡ i)<br>when checking that the type ... of the generated with function is well-formed</div><div><br></div><div>I'm wondering, is there a way to manually do the rewrite? The problem is that "decEq i i" doesn't actually appear in the type, it's just what the evaluation gets stuck on, so I don't think I can use subst. Basically, other than rewrite (which is failing), I don't know how to tell Agda the value of a term that normalization is stuck on.</div><div><br></div><div>Thanks!<br></div></div>