<div dir="ltr"><div dir="ltr"><div dir="ltr"><div dir="ltr"><div dir="ltr">Hi-<div><br></div><div>     I have a question about proving inequalities (≢) in Agda. It's probably such a stupid question that I should be embarrassed for asking it, but, fortunately, I lost my capacity to feel embarrassment years ago. </div><div><br></div><div><font face="arial, sans-serif">In the following Agda code, the "good" definition works, but the "bad" one does not and yields the commented complaint. I assume that <span style="color:rgb(0,0,0)">(≢)</span><span style="color:rgb(0,0,0)"> insists on literal term equality and that is the source of the different responses from Agda. Is there any way of evaluating under the </span><span style="color:rgb(0,0,0)">(≢)? I'm formulating a typed language using strings for variables, and so this sort of inequality calculation is involving in variable dereference. I've attached a minimal example. Thanks in advance.</span></font></div><div><div><br></div></div></div></div><blockquote style="margin:0px 0px 0px 40px;border:none;padding:0px"><div><div><div><div>good : "x" ≢ "y"</div></div></div></div><div><div><div><div>good ()</div></div></div></div><div><div><div><div><br></div></div></div></div><div><div><div><div>bad : "x" ≢ Data.Vec.head ("y" ∷ "y" ∷ []) </div></div></div></div><div><div><div><div>bad ()</div></div></div></div><div><div><div><div><br></div></div></div></div><div><div><div><div>{-</div></div></div></div><div><div><div><div>Failed to solve the following constraints:</div></div></div></div><div><div><div><div>  Is empty: "x" ≡ head ("y" ∷ "y" ∷ [])</div></div></div></div><div><div><div><div>      [ at <...snip...>/MinimalExample.agda:11,5-7 ]</div></div></div></div><div><div><div><div>-}</div></div></div></div></blockquote><div dir="ltr"><div dir="ltr"><div><br></div></div></div></div></div></div>