X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Flib%2Fturing%2Funiversal%2Falphabet.ma;h=bf2484f29fadf94ae268dc9a7dad93ec54bfafac;hb=0460fd3dc2909efe0baa6592281d0cf0527165ff;hp=04701aeec180b8b868e7388f186cb173900bb2ef;hpb=67948c54e4e20ef530d2d2115c9a056275360012;p=helm.git

diff --git a/matita/matita/lib/turing/universal/alphabet.ma b/matita/matita/lib/turing/universal/alphabet.ma
index 04701aeec..bf2484f29 100644
--- a/matita/matita/lib/turing/universal/alphabet.ma
+++ b/matita/matita/lib/turing/universal/alphabet.ma
@@ -39,10 +39,18 @@ definition DeqUnialpha ≝ mk_DeqSet unialpha unialpha_eq ?.
   |*: * [1,6,11,16: #y ] normalize % #H1 destruct % ]
 qed.
 
-axiom unialpha_unique : uniqueb DeqUnialpha [bit true;bit false;comma;bar;grid] = true.
+lemma unialpha_unique : 
+  uniqueb DeqUnialpha [bit true;bit false;null;comma;bar;grid] = true.
+// qed.
+
+lemma unialpha_complete :∀x:DeqUnialpha. 
+  memb ? x [bit true;bit false;null;comma;bar;grid] = true.
+* // * //
+qed.
 
 definition FSUnialpha ≝ 
-  mk_FinSet DeqUnialpha [bit true;bit false;null;comma;bar;grid] unialpha_unique.
+  mk_FinSet DeqUnialpha [bit true;bit false;null;comma;bar;grid] 
+  unialpha_unique unialpha_complete.
 
 definition is_bit ≝ λc.match c with [ bit _ ⇒ true | _ ⇒ false ].