X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=inline;f=matita%2Fmatita%2Flib%2Flambda%2Fsubterms.ma;h=d2b7bee30b76c7fe82e634bd3d15e732f1aff629;hb=ffbc6cd1358d61072105766052c7498a1f37c769;hp=86d95b64371372def606dc062c6b73afc9fde832;hpb=565ece080269f1d602d239a54bc68fdc6ad52c33;p=helm.git

diff --git a/matita/matita/lib/lambda/subterms.ma b/matita/matita/lib/lambda/subterms.ma
index 86d95b643..d2b7bee30 100644
--- a/matita/matita/lib/lambda/subterms.ma
+++ b/matita/matita/lib/lambda/subterms.ma
@@ -139,7 +139,7 @@ match M with
   ]
 .
 
-axiom pos_size: ∀M. 1 ≤ size M.
+(* axiom pos_size: ∀M. 1 ≤ size M. *)
 
 theorem Telim_size: ∀P: T → Prop. 
  (∀M. (∀N. size N < size M → P N) → P M) → ∀M. P M.
@@ -148,3 +148,9 @@ theorem Telim_size: ∀P: T → Prop.
 #p @(nat_elim1 p) #m #H1 #N #sizeN @H #N0 #Hlt @(H1 (size N0)) //
 qed.
 
+(* size of subterms *)
+
+lemma size_subterm : ∀N,M. subterm N M → size N < size M.
+#N #M #subH (elim subH) normalize //
+#M1 #N1 #P #sub1 #sub2 #size1 #size2 @(transitive_lt … size1 size2)
+qed.