如何在Coq中的类的属性中使用表示为列表的有限集？

Require Import List.

Class FiniteSet (A:Type) :=
{
  set : list A;
  add : A -> list A -> list A;
  remove : A -> list A -> list A;
  contains : A -> list A -> bool
}.

Definition add_impl {A:Type} `{FiniteSet A} (x:A) (s:list A) :=
  x::s.

Definition remove_impl {A:Type} `{FiniteSet A} (x:A) (s:list A) :=
  filter (fun y => negb (x =? y)) s.

Definition contains_impl {A:Type} `{FiniteSet A} (x:A) (s:list A) :=
  existsb (x =?) s.

Lemma add_spec : forall (A:Type) `{FiniteSet A} (x:A) (s:list A),
  contains x (add x s) = true.
Proof.
  intros. unfold contains_impl, add_impl.
  rewrite existsb_exists. exists x.
  split.
  - apply Nat.eqb_refl.
  - apply in_eq.
Qed.

(* 其他操作和规范的定义类似，这里省略 *)

(* 创建一个有限集类型的实例 *)
Instance NatSet : FiniteSet nat :=
{
  set := nil;
  add := add_impl;
  remove := remove_impl;
  contains := contains_impl
}.

(* 在主程序中使用 *)
Definition mySet := add 42 (add 10 set).
Compute contains 42 mySet.