New notation for congruence

[helm.git] / matita / matita / lib / turing / universal / alphabet.ma

diff --git a/matita/matita/lib/turing/universal/alphabet.ma b/matita/matita/lib/turing/universal/alphabet.ma
index 4d87907d23130f1a6937a99ccd0d3df371bc9b31..390bc2b839d308a6222816fc9d479e6edb3999b1 100644 (file)
--- 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.