unistep!!!

[helm.git] / matita / matita / lib / turing / multi_universal / normalTM.ma

diff --git a/matita/matita/lib/turing/multi_universal/normalTM.ma b/matita/matita/lib/turing/multi_universal/normalTM.ma
index 8e3af494a032715a3f6f90affcfd77770549aa9a..6459cedd9590e282e642f62e40b880bd599c40ae 100644 (file)
--- a/matita/matita/lib/turing/multi_universal/normalTM.ma
+++ b/matita/matita/lib/turing/multi_universal/normalTM.ma
@@ -205,6 +205,18 @@ definition low_mv ≝ λm.
   | N ⇒ null
   ].
 
+lemma injective_low_char: injective … low_char.
+#c1 #c2 cases c1 cases c2 normalize //
+  [#b1 #H destruct
+  |#b1 #H destruct
+  |#b1 #b2 #H destruct //
+  ]
+qed.   
+
+lemma injective_low_mv: injective … low_mv.
+#m1 #m2 cases m1 cases m2 // normalize #H destruct
+qed.
+   
 (******************************** tuple encoding ******************************)
 definition tuple_type ≝ λn.
  (Nat_to n × (option FinBool)) × (Nat_to n × (option FinBool) × move).