proposition: Lemma finite_inter : forall P Q, dec P -> finite Q -> finite (inter P Q).
proof: Proof. intros P Q decP FQ. induction FQ. constructor 1. apply equiv_trans with (inter P empty); auto. case (decP x); intro. constructor 2 with x (inter P Q); auto. unfold inter; intuition. rewrite e. unfold add,inter; red; intuition. subst; auto. apply fin_equiv with (inter P Q); auto. rewrite e. unfold add,inter; red; intuition. subst; intuition. Defined.
imports: Coq(Arith) Coq(Lt)