proposition: Lemma set_add_intro2 : forall (a b:A) (x:set), a = b -> set_In a (set_add b x).
proof: Proof. unfold set_In; simple induction x; simpl. - auto with datatypes. - intros a0 l H Hab. elim (Aeq_dec b a0); [ rewrite Hab; intro Hba0; rewrite Hba0; simpl; auto with datatypes | auto with datatypes ]. Qed.
imports: List