Splitted re into lang.ma nd re.ma

[helm.git] / matita / matita / lib / re / moves.ma

diff --git a/matita/matita/lib/re/moves.ma b/matita/matita/lib/re/moves.ma
index b7f094d867183b0dddde020dd1783f6394e0edf8..4967bf0596ddf7ec35fecebd29d8460761247e2e 100644 (file)
--- a/matita/matita/lib/re/moves.ma
+++ b/matita/matita/lib/re/moves.ma
@@ -304,6 +304,7 @@ lemma notb_eq_true_l: ∀b. notb b = true → b = false.
 #b cases b normalize //
 qed.
 
+(*
 lemma notb_eq_true_r: ∀b. b = false → notb b = true.
 #b cases b normalize //
 qed.
@@ -314,7 +315,7 @@ qed.
 
 lemma notb_eq_false_r:∀b. b = true → notb b = false.
 #b cases b normalize //
-qed.
+qed. *)
 
 (* include "arithmetics/exp.ma". *)