proposition: Lemma add_part_simpl : forall (A B : part_set E) (x : E), ~ in_part x A -> ~ in_part x B -> Equal (add_part A x) (add_part B x) -> Equal A B.
proof: Proof. intros A B. case A; case B; simpl in |- *. intros a pa b pb. unfold eq_part, add_part, union, single in |- *; simpl in |- *. intros. elim (classic (Equal x x0)); intros. split; intros. apply pa with x; auto with algebra. cut (b x). intro. absurd (b x); auto with algebra. apply pb with x0; auto with algebra. cut (a x). intro. absurd (a x); auto with algebra. apply pa with x0; auto with algebra. elim (H1 x0); intros. split; intros. lapply H3. intros. elim H6; intros. auto with algebra. absurd (Equal x0 x); auto with algebra. left; auto with algebra. lapply H4; intros. elim H6; intros. auto with algebra. absurd (Equal x0 x); auto with algebra. left. auto with algebra. Qed.
imports: Union Singleton Diff Classical_Prop