| Dealing with Set-level specifications |
Set Implicit Arguments.
Definition sum_to_bool (A B : Prop) (p : {A} + {B}) :=
if p then true else false.
Inductive pred_option (P : Prop) : Set :=
| PSome : P -> pred_option P
| PNone : pred_option P.
Definition popt_to_bool P (po : pred_option P) :=
match po with
| PNone => false
| _ => true
end.
Lemma popt_to_bool_true : forall P (po : pred_option P),
popt_to_bool po = true
-> P.
Definition popt_Prop P (po : pred_option P) :=
match po with
| PNone => False
| _ => True
end.
Inductive sig_option (T : Set) (P : T -> Prop) : Set :=
| SSome : forall x, P x -> sig_option P
| SNone : sig_option P.