proposition: Lemma size_inter_incl : forall P Q (decP:dec P)(FP:finite P)(FQ:finite Q), (incl P Q) -> size (finite_inter decP FQ)=size FP.
proof: Proof. intros; apply size_unique. unfold inter; intro. generalize (H x); intuition. Qed.
imports: Coq(Arith) Coq(Lt)