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.