proposition: Lemma single_law : forall x y : E, Equal x y -> Equal (single x) (single y).
proof: Proof. unfold single in |- *; simpl in |- *. unfold eq_part in |- *; simpl in |- *. intros x y H' x0; split; [ intros H'0; try assumption | idtac ]. apply Trans with x; auto with algebra. intros H'0; try assumption. apply Trans with y; auto with algebra. Qed.
imports: Parts