<div dir="ltr"><div><div><div><div><div><div><div>Currently, instance resolution tries all possible ways to construct an instance argument.<br><br></div>It will look for arguments in the environment and it will use instance functions to create new ones. If there are multiple solutions, instance resolution will fail.<br><br></div>example :</div><div><br></div><div> Assuming we have defined "less than" as instance.<br><br></div>if we have in the context, a variable q with type zero ≤ (suc zero) , instance resolution will fail because there are two solutions, q and z≤n.<br></div><br></div>But q is  in fact z≤n.<br><br><br></div>We can prove that there is only one possible construction of the type, thus any variables with the same type are the same.<br></div><div><br></div><div>At the moment, I am trying to prune my context but it would be nice if instance resolution was a bit smarter.<br></div></div>