Library Coq.Bool.DecBool
Set Implicit Arguments
.
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
.
Unset Implicit Arguments
.