proposition: Lemma set_add_elim : forall (a b:A) (x:set), set_In a (set_add b x) -> a = b \/ set_In a x.
proof: Proof. unfold set_In. simple induction x. - simpl; intros [H1| H2]; auto with datatypes. - simpl; do 3 intro. elim (Aeq_dec b a0). + simpl; tauto. + simpl; intros H0 [|]. * trivial with datatypes. tauto. * tauto. Qed.
imports: List