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”.