Fine-tuning rewriting from "eq_true b": using <- to rewrite true to b

(if ever necessary).


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11621 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 18 insertions, 2 deletions

diff --git a/theories/Init/Datatypes.v b/theories/Init/Datatypes.v
index 45228073a..beda128af 100644
--- a/theories/Init/Datatypes.v
+++ b/theories/Init/Datatypes.v
@@ -72,9 +72,25 @@ Hint Resolve andb_true_intro: bool v62.
 
 Inductive eq_true : bool -> Prop := is_eq_true : eq_true true.
 
-(** Technical lemma: identify -> rewriting on eq_true with <- rewriting *)
+(** Additional rewriting lemmas about [eq_true] *)
 
-Definition eq_true_ind_r := eq_true_ind.
+Lemma eq_true_ind_r :
+  forall (P : bool -> Prop) (b : bool), P b -> eq_true b -> P true.
+Proof.
+  intros P b H H0; destruct H0 in H; assumption.
+Defined.
+
+Lemma eq_true_rec_r :
+  forall (P : bool -> Set) (b : bool), P b -> eq_true b -> P true.
+Proof.
+  intros P b H H0; destruct H0 in H; assumption.
+Defined.
+
+Lemma eq_true_rect_r :
+  forall (P : bool -> Type) (b : bool), P b -> eq_true b -> P true.
+Proof.
+  intros P b H H0; destruct H0 in H; assumption.
+Defined.
 
 (** [nat] is the datatype of natural numbers built from [O] and successor [S];
     note that the constructor name is the letter O.