- lambda_notation.ma: more notation and bug fixes

[helm.git] / matita / matita / lib / lambda / subterms.ma

diff --git a/matita/matita/lib/lambda/subterms.ma b/matita/matita/lib/lambda/subterms.ma
index 86d95b64371372def606dc062c6b73afc9fde832..d2b7bee30b76c7fe82e634bd3d15e732f1aff629 100644 (file)
--- 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.