X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Flib%2Fturing%2Fmulti_universal%2Funiversal.ma;fp=matita%2Fmatita%2Flib%2Fturing%2Fmulti_universal%2Funiversal.ma;h=9b245cde9216b449d1aa2219c402a2d52b8113dd;hb=d7d92f459cf6d76051c255497ee1ca898b111b76;hp=e371e4d909c340d0591ed2356c505ed63fce9612;hpb=10bb008413e04d44051590a8069e4f16f6f56102;p=helm.git

diff --git a/matita/matita/lib/turing/multi_universal/universal.ma b/matita/matita/lib/turing/multi_universal/universal.ma
index e371e4d90..9b245cde9 100644
--- a/matita/matita/lib/turing/multi_universal/universal.ma
+++ b/matita/matita/lib/turing/multi_universal/universal.ma
@@ -10,9 +10,7 @@
       V_____________________________________________________________*)
 
 include "turing/simple_machines.ma".
-include "turing/multi_universal/unistep_aux.ma".
-
-axiom sem_unistep: ∀M. unistep ⊨ R_unistep_high M.
+include "turing/multi_universal/unistep.ma".
 
 definition stop ≝ λc.
   match c with [ bit b ⇒ notb b | _ ⇒ true].