freescale porting, work in progress

[helm.git] / helm / software / matita / contribs / ng_assembly / test_errori.ma

diff --git a/helm/software/matita/contribs/ng_assembly/test_errori.ma b/helm/software/matita/contribs/ng_assembly/test_errori.ma
index 921c1b505a26636a662551ab407f055db1d3c22a..4236c5c6341f7c0b93e878951e88b04880244284 100644 (file)
--- a/helm/software/matita/contribs/ng_assembly/test_errori.ma
+++ b/helm/software/matita/contribs/ng_assembly/test_errori.ma
@@ -1,28 +1,4 @@
 
-(* congettura, come si fa? *)
-include "num/exadecim.ma".
-include "num/exadecim_lemmas.ma".
-
-nlemma decidable_ex_aux1 : ∀x.∀H:x0 = x.(x0 = x) ∨ (x0 ≠ x).
- #x; nelim x;
- ##[ ##1: #H; napply (or_introl … H)
- ##| ##*: #H; nelim (exadecim_destruct … H)
- ##]. nqed.
-
-nlemma decidable_ex0 : ∀x:exadecim.decidable (x0 = x).
- #x;
- nelim x;
- nnormalize;
- napply (Or_ind (x0=x) (x0≠x) ? ? …);
- ##[ ##1: napply (or_introl (x0 = x0) (x0 ≠ x0) (refl_eq …))
- ##| ##*:
- 
- nnormalize;
- nelim x;
- ##[ ##1: nelim y;
-          ##[ ##1: napply (or_introl (? = ?) (? ≠ ?) (refl_eq …))
-          ##| ##*:
-
 (*include "utility/utility.ma".
 
 nlemma fold_right_neList2_aux3 :