X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=matita%2Fmatita%2Flib%2Fpts_dummy_new%2Farity.ma;h=b5dd81df710cd84e4627e9a5dd04093a27be283d;hb=b4f76b0d8fa0e5365fb48e91474febe200b647a7;hp=3df7811c060e003335a8f36fb3dc3ac0badfc7cc;hpb=46e87acb755894f9234191d675eeb5db4f5b930b;p=helm.git

diff --git a/matita/matita/lib/pts_dummy_new/arity.ma b/matita/matita/lib/pts_dummy_new/arity.ma
index 3df7811c0..b5dd81df7 100644
--- a/matita/matita/lib/pts_dummy_new/arity.ma
+++ b/matita/matita/lib/pts_dummy_new/arity.ma
@@ -12,8 +12,8 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "lambda/ext.ma".
-
+include "pts_dummy/ext.ma".
+(*
 (* ARITIES ********************************************************************)
 
 (* An arity is a normal term representing the functional structure of a term.
@@ -218,3 +218,4 @@ lemma nth_sort_comp: ∀E1,E2. E1 ≅ E2 →
                      ∀i. nth i ? E1 sort ≅ nth i ? E2 sort.
 #E1 #E2 #H #i @(all2_nth … aeq) //
 qed.
+*)