proposition: Lemma fin_equiv: forall (P Q : set), (equiv P Q)->(finite P)->(finite Q).
proof: Proof. induction 2. apply fin_eq_empty. apply equiv_trans with P; auto. apply fin_eq_add with x Q0; auto. apply equiv_trans with P; auto. Defined.
imports: Coq(Arith) Coq(Lt)