Library Coq.Bool.DecBool
Definition ifdec (
A B:
Prop) (
C:
Type) (
H:
{A} + {B}) (
x y:
C) :
C :=
if H then x else y.
Theorem ifdec_left :
forall (
A B:
Prop) (
C:
Set) (
H:
{A} + {B}),
~ B ->
forall x y:
C,
ifdec H x y = x.
Theorem ifdec_right :
forall (
A B:
Prop) (
C:
Set) (
H:
{A} + {B}),
~ A ->
forall x y:
C,
ifdec H x y = y.