1 files changed, 3 insertions, 1 deletions
diff --git a/theories/Bool/Bool.v b/theories/Bool/Bool.v
index 7f8f52c4f6..ab1a4b9e04 100755
--- a/theories/Bool/Bool.v
+++ b/theories/Bool/Bool.v
@@ -106,6 +106,7 @@ 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 .
@@ -121,7 +122,8 @@ Intros H.
 Inversion_clear H.
 Trivial with bool.
 Save.
- 
+*****)
+
 Lemma eqb_reflx : (b:bool)(eqb b b)=true.
 Intro b.
 Case b.