proposition: Lemma set_mem_ind2 : forall (B:Type) (P:B -> Prop) (y z:B) (a:A) (x:set), (set_In a x -> P y) -> (~ set_In a x -> P z) -> P (if set_mem a x then y else z).
proof: Proof. simple induction x; simpl; intros. - apply H0; red; trivial. - case (Aeq_dec a a0); auto with datatypes. intro Hneg; apply H; intros; auto. apply H1; red; intro. case H3; auto. Qed.
imports: List