urgent partial commit ... to be fixed later ...

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

diff --git a/matita/matita/contribs/lambda_delta/basic_2/unfold/tpss.ma b/matita/matita/contribs/lambda_delta/basic_2/unfold/tpss.ma
index 707e469596d8d1a2213280446efc597b7b8fd557..fc74d802ca9a48c1f790a4db731287a990be849c 100644 (file)
--- a/matita/matita/contribs/lambda_delta/basic_2/unfold/tpss.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/unfold/tpss.ma
@@ -144,3 +144,12 @@ lemma tpss_inv_refl_O2: ∀L,T1,T2,d. L ⊢ T1 [d, 0] ▶* T2 → T1 = T2.
 | #T #T2 #_ #HT2 #IHT <(tps_inv_refl_O2 … HT2) -HT2 //
 ]
 qed-.
+
+(* Basic forward lemmas *****************************************************)
+
+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
+@(transitive_le … IHT1) //
+qed-.