Proved old axiom.

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / unfold / tpss.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_2/unfold/tpss.ma b/matita/matita/contribs/lambdadelta/basic_2/unfold/tpss.ma
index 93916208b649a6d301c53ab4ef1e56f9d6417871..cc5be0ecab230655c2413f42211b41c8f6201057 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/unfold/tpss.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/unfold/tpss.ma
@@ -164,7 +164,7 @@ qed-.
 
 (* Basic forward lemmas *****************************************************)
 
-lemma tpss_fwd_tw: ∀L,T1,T2,d,e. L ⊢ T1 ▶* [d, e] T2 → #{T1} ≤ #{T2}.
+lemma tpss_fwd_tw: ∀L,T1,T2,d,e. L ⊢ T1 ▶* [d, e] T2 → ♯{T1} ≤ ♯{T2}.
 #L #T1 #T2 #d #e #H @(tpss_ind … H) -T2 //
 #T #T2 #_ #HT2 #IHT1
 lapply (tps_fwd_tw … HT2) -HT2 #HT2