X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Flib%2Fturing%2Funiversal%2Falphabet.ma;h=390bc2b839d308a6222816fc9d479e6edb3999b1;hb=225887a9f23aac79d4cca907da026917b7df04dc;hp=4d87907d23130f1a6937a99ccd0d3df371bc9b31;hpb=cd7e658c917c4542b0308acf208aa40f1f7064e4;p=helm.git

diff --git a/matita/matita/lib/turing/universal/alphabet.ma b/matita/matita/lib/turing/universal/alphabet.ma
index 4d87907d2..390bc2b83 100644
--- a/matita/matita/lib/turing/universal/alphabet.ma
+++ b/matita/matita/lib/turing/universal/alphabet.ma
@@ -80,6 +80,12 @@ qed.
 lemma bit_or_null_not_bar: ∀d. bit_or_null d = true → is_bar d = false.
 * // normalize #H destruct
 qed.
+
+lemma is_bit_to_bit_or_null : 
+  ∀x.is_bit x = true → bit_or_null x = true.
+* // normalize #H destruct
+qed.
+
 (**************************** testing strings *********************************)
 definition is_marked ≝ λalpha.λp:FinProd … alpha FinBool.
   let 〈x,b〉 ≝ p in b.