proposition: Lemma set_mem_ind : forall (B:Type) (P:B -> Prop) (y z:B) (a:A) (x:set), (set_In a x -> P y) -> P z -> P (if set_mem a x then y else z).
proof: Proof. simple induction x; simpl; intros. - assumption. - elim (Aeq_dec a a0); auto with datatypes. Qed.
imports: List