proposition: Lemma fold_add_spec s1 s2 x : InT x (fold add s1 s2) <-> InT x s1 \/ InT x s2.
proof: Proof. rewrite fold_spec, <- fold_left_rev_right. rewrite <- (elements_spec1 s1), <- InA_rev by auto_tc. unfold elt in *. induction (rev (elements s1)); simpl. - rewrite InA_nil. tauto. - unfold flip. rewrite add_spec', IHl, InA_cons. tauto. Qed.
imports: Bool List BinPos Pnat Setoid SetoidList PeanoNat