proposition: Lemma set_rec: forall (P:t->Type), (forall s s', equal s s'=true -> P s -> P s') -> (forall s x, mem x s=false -> P s -> P (add x s)) -> P empty -> forall s, P s.
proof: Proof. intros. apply set_induction; auto; intros. - apply X with empty; auto with set. - apply X with (add x s0); auto with set. + apply equal_1; intro a; rewrite add_iff; rewrite (H0 a); tauto. + apply X0; auto with set; apply mem_3; auto. Qed.
imports: MSetProperties Zerob Sumbool Lia DecidableTypeEx