proposition: Lemma fold_remove_spec s1 s2 x `(Ok s2) : InT x (fold remove s1 s2) <-> InT x s2 /\ ~InT x s1.
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; intros. - rewrite InA_nil. intuition. - unfold flip in *. rewrite remove_spec, IHl, InA_cons. + tauto. + clear IHl. induction l; simpl; auto_tc. Qed.
imports: Bool List BinPos Pnat Setoid SetoidList PeanoNat