proposition: Lemma size_inter_add_in : forall P Q R (decP:dec P)(x:A)(nq:~Q x)(FQ:finite Q)(e:equiv R (add x Q)), P x ->size (finite_inter decP (fin_eq_add nq FQ e))=S (size (finite_inter decP FQ)).
proof: Proof. intros; simpl. case (decP x); intro; trivial; contradiction. Qed.
imports: Coq(Arith) Coq(Lt)