proposition: Lemma single_simpl : forall x y : E, Equal (single x) (single y) -> Equal x y.
proof: Proof. simpl in |- *. unfold eq_part, single in |- *; simpl in |- *. intros x y H'; try assumption. elim (H' x); auto with algebra. Qed.
imports: Parts