comparator should permit dependent challenges ("Const does not match" is sometimes a lie)

Consider the challenge
```lean
theorem foo : 1 = 1 := sorry
theorem bar : foo = foo := sorry
```
with solution
```lean
theorem foo : 1 = 1 := Eq.refl _
theorem bar : foo = foo := Eq.refl _
```
comparator tells me that foo is a valid solution, but if I tell it that it should be comparing both foo and bar, it tells me `uncaught exception: Const does not match between challenge and target 'foo'`