Coq：定义子类型

我有一个类型，比如说

Inductive Tt := a | b | c.

定义它的子类型的最简单和/或最好的方法是什么？假设我希望子类型仅包含构造函数a and b。一种方法是对二元素类型进行参数化，例如布尔：

Definition filt (x:bool): Tt := match x with
  | true => a
  | false => b end.
Check filt true: Tt.

这是可行的，但如果您的表达式具有以这种方式定义的多个（可能相互依赖的）子类型，则非常尴尬。此外，它只能工作一半，因为没有定义子类型。为此，我必须另外定义例如

Notation _Tt := ltac: (let T := type of (forall {x:bool}, filt x) in exact T).
Fail Check a: _Tt. (*The term "filt x" has type "Tt" which should be Set, Prop or Type.*)

在这种情况下也不起作用。另一种方法是使用类型类，例如

Class s_Tt: Type := s: Tt.
Instance a':s_Tt := a.
Instance b':s_Tt := b.
Check a: s_Tt.
Check b': Tt.
Check c: s_Tt.

如您所见，这是行不通的：c仍然在s_Tt（即使类型推断应该在实例中工作得更好）。最后来个强制

Parameter c0:> bool -> Tt.
Notation a_ := true.
Notation b_ := false.
Notation Tt_ := bool.
Check a_: Tt_.
Check b_: Tt.
Fail Check a: Tt_.

有效，但是，当然，a and b不能用作已定义子类型的术语（这总是很方便，有时也是必要的）

我认为子集类型不应该是这个问题的答案（子集类型的术语永远不是其（适当的）超集的术语）。也许有更好的方法来使用类型类来达到此目的？