This demonstrates that a list-based agreement could work, and form an OFE. I didn't bother to prove all the functor laws.
Man, this reasoning with about the lists is annoying^^.
What I don't like about this is that un-injection (agree_car) is only non-expansive for valid elements. I want to try using a different equivalence relation, maybe I can find one where this works.