The Coq mailing list

[Arthur Azevedo de Amorim <arthur.aa AT gmail.com>]

Hello,

I am having a problem using the new rewriting system in Coq 8.2. First, I declared a basic setoid record
with a carrier, a relation and a proof that this relation is an equivalence relation. Then I declared a new type
for maps between setoids (A =>> B), that have a function and a proof that it preserves equality. I added the equality
and these maps as relations and morphisms, and then added a canonical structure for seeing a setoid morphism
with a setoid structure. So far so good. The problem appears when I try to curry this scheme: if I have F : A =>> B =>> C,
I can't proof that a1 == a2 -> F a1 b == F a2 b unless I destruct F explicitly and apply the preservation lemma
it carries. Is there a way of doing this with a regular rewrite?

-- 
Arthur Azevedo de Amorim