proposition: Lemma inj_part_included_injective : forall (A B : part_set E) (p : included A B), injective (inj_part_included p).
proof: Proof. intros A B p; red in |- *. intros x y; try assumption. elim x. elim y. simpl in |- *; auto with algebra. Qed.
imports: Sets