proposition: Lemma cart_eq_equiv : equivalence cart_eq.
proof: Proof. red in |- *. split; [ try assumption | idtac ]. red in |- *. intros x; red in |- *. elim x. unfold cart_eq in |- *; simpl in |- *; auto with algebra. red in |- *. split; [ idtac | try assumption ]. red in |- *. unfold app_rel, cart_eq in |- *. intros x y z H' H'0; split; [ try assumption | idtac ]. apply Trans with (cart_l y); intuition. apply Trans with (cart_r y); intuition. red in |- *. unfold app_rel, cart_eq in |- *. intuition. Qed.
imports: Sets