diff options
Diffstat (limited to 'theories/Bool/Bool.v')
| -rwxr-xr-x | theories/Bool/Bool.v | 2 |
1 files changed, 0 insertions, 2 deletions
diff --git a/theories/Bool/Bool.v b/theories/Bool/Bool.v index 7737c4837..c49c4bf8e 100755 --- a/theories/Bool/Bool.v +++ b/theories/Bool/Bool.v @@ -106,7 +106,6 @@ Lemma Is_true_eq_true2 : (x:bool) x=true -> (Is_true x). Destruct x; Simpl; Auto with bool. Save. -(***** TODO Lemma eqb_subst : (P:bool->Prop)(b1,b2:bool)(eqb b1 b2)=true->(P b1)->(P b2). Unfold eqb . @@ -122,7 +121,6 @@ Intros H. Inversion_clear H. Trivial with bool. Save. -*****) Lemma eqb_reflx : (b:bool)(eqb b b)=true. Intro b. |