proposition: Lemma Crel_strext (R: relation T): Proper (equiv ==> equiv ==> iff) R -> Crel_strext CSetoid R.
proof: Proof. Proof with auto. red. simpl. intros. destruct (eq_dec x1 x2)... destruct (eq_dec y1 y2)... left. rewrite <- e, <- e0... Qed.
imports: CoRN.algebra.CSetoids Coq.Classes.SetoidDec Coq.Classes.Morphisms Coq.Classes.SetoidClass