-lemma xxx : ∀x.carr x → carr1 (setoid1_of_setoid x). intros; assumption; qed.
-coercion xxx nocomposites.
-
-lemma down_p : ∀S,I:SET.∀u:S⇒S.∀c:arrows1 SET I S.∀a:I.∀a':I.a=a'→u (c a)=u (c a').
-intros; unfold uncurry_arrows; change in c with (I ⇒ S);
-apply (†(†H));