Consider the following three definitions, where f3 doesn’t typecheck:

```
Inductive function_true : Prop := mk_function_true.
Inductive function_false : Prop := mk_function_false.
Definition function_pred (b : bool) : Prop :=
match b with
| true => function_true
| false => function_false
end.
Definition f1 (p : function_pred true) : unit :=
match p with
| mk_function_true => tt
end.
Inductive family_set : bool -> Set :=
| family_set_true : family_set true
| family_set_false : family_set false.
Definition f2 (p : family_set true) : unit :=
match p with
| family_set_true => tt
end.
Inductive family_pred : bool -> Prop :=
| family_true : family_pred true
| family_false : family_pred false.
Definition f3 (p : family_pred true) : unit :=
match p with
| family_true => tt
end.
```

It seems like morally f1 and f3 are doing the same thing. I understand that under the hood the return type of the match in f2 and f3 is (if b then unit else IDProp), but even with that is there any reason f3 couldn’t be accepted here?

To be clear, the condition I’m looking for is “if P : Prop is effectively a singleton once its known indices are taken into account, we can eliminate into Set/Type”.