[Agda] Re: reflective access to definitional equality

[Stefan Monnier]

> I was getting sick of proving equations like

> pf : (x y z : Bool) -> Id (contains y (x :: (y :: (z :: [])))) True

> (or of writing out a reflection goal and instantiating it with the
> current context).
> So, I thought, what if I could write contains in such a way that the
> above reduced to True *definitionally*?

Indeed, that could solve it here.  I even dream of such a thing
happening without having to explicitly use a "testDefEq", instead "just"
by making the normalization stronger.
After all, compilers do such optimizations everyday.


        Stefan