Library Coq.Bool.IfProp
Require
Import
Bool
.
Inductive
IfProp
(
A
B
:Prop) :
bool
->
Prop
:=
|
Iftrue
:
A
->
IfProp
A
B
true
|
Iffalse
:
B
->
IfProp
A
B
false
.
Hint
Resolve
Iftrue
Iffalse
:
bool
v62
.
Lemma
Iftrue_inv
:
forall
(
A
B
:Prop) (
b
:bool),
IfProp
A
B
b
->
b
=
true
->
A
.
Lemma
Iffalse_inv
:
forall
(
A
B
:Prop) (
b
:bool),
IfProp
A
B
b
->
b
=
false
->
B
.
Lemma
IfProp_true
:
forall
A
B
:Prop,
IfProp
A
B
true
->
A
.
Lemma
IfProp_false
:
forall
A
B
:Prop,
IfProp
A
B
false
->
B
.
Lemma
IfProp_or
:
forall
(
A
B
:Prop) (
b
:bool),
IfProp
A
B
b
->
A
\/
B
.
Lemma
IfProp_sum
:
forall
(
A
B
:Prop) (
b
:bool),
IfProp
A
B
b
-> {
A
} + {
B
}.