proposition: Lemma set_add_intro1 : forall (a b:A) (x:set), set_In a x -> set_In a (set_add b x).
proof: Proof. unfold set_In; simple induction x; simpl. - auto with datatypes. - intros a0 l H [Ha0a| Hal]. + elim (Aeq_dec b a0); left; assumption. + elim (Aeq_dec b a0); right; [ assumption | auto with datatypes ]. Qed.
imports: List