proposition: Lemma in_part_trans_eq : forall (A : part_set E) (x y : E), in_part x A -> Equal y x -> in_part y A.
proof: Proof. intros A; case A; simpl in |- *. intros a pa. intros x y H' H'0; try assumption. apply pa with x; auto with *. Qed.
imports: Fpart Inter Arith