X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fng_assembly%2Ftest_errori.ma;h=4236c5c6341f7c0b93e878951e88b04880244284;hb=a62de71cf6821c955bd41fa691c52ea62173f25d;hp=921c1b505a26636a662551ab407f055db1d3c22a;hpb=17e7978cda0dfa4585393b0c48bd96e9504a6b92;p=helm.git

diff --git a/helm/software/matita/contribs/ng_assembly/test_errori.ma b/helm/software/matita/contribs/ng_assembly/test_errori.ma
index 921c1b505..4236c5c63 100644
--- 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 :