Yのセットが別のセットXのサブセットであることをCoqでどのように記述できますか？Coqでサブセット関係を表現するには？
私は次のようにテストした：
Definition subset (Y X:Set) : Prop :=
forall y:Y, y:X.
、要素yがYである場合、その後、yがXであることを表現しようとしています。しかし、これは驚くことではないが、yについてのタイプエラーを生成する。
Coqでsubsetを定義する簡単な方法はありますか？ここで
は、それが標準ライブラリ（Coq.Logic.ClassicalChoice）で行われる方法です。
Definition subset (U:Type) (P Q:U->Prop) : Prop := forall x, P x -> Q x.
単項述語PとQは、（ユニバーサル）のいくつかのサブセットを表すUを設定するので、上記の定義が読み取りますたびに、いくつかのxをPにあると同時に、Qにあります。
幾分類似defintionはCoq.MSets.MSetInterfaceに見出すことができる：
Inタイプ
eltいくつかの要素がタイプ
tのセットのメンバであることを意味し、
elt -> t -> Prop型を持つ
Definition Subset s s' := forall a : elt, In a s -> In a s'.
。