old pr2_subst1 (Basic-1) closed!

[helm.git] / matita / matita / contribs / lambda_delta / Basic_2 / reduction / ltpr.ma

diff --git a/matita/matita/contribs/lambda_delta/Basic_2/reduction/ltpr.ma b/matita/matita/contribs/lambda_delta/Basic_2/reduction/ltpr.ma
index 9cbd3d6c8fc57a09788cf02838fac19ff46cb6e1..b7a01f3df4a933a3883c044d4cba6aca86dbaa62 100644 (file)
--- a/matita/matita/contribs/lambda_delta/Basic_2/reduction/ltpr.ma
+++ b/matita/matita/contribs/lambda_delta/Basic_2/reduction/ltpr.ma
@@ -80,4 +80,10 @@ lemma ltpr_inv_pair2: ∀L1,K2,I,V2. L1 ⇒ K2. 𝕓{I} V2 →
                       ∃∃K1,V1. K1 ⇒ K2 & V1 ⇒ V2 & L1 = K1. 𝕓{I} V1.
 /2/ qed.
 
+(* Basic forward lemmas *****************************************************)
+
+lemma ltpr_fwd_length: ∀L1,L2. L1 ⇒ L2 → |L1| = |L2|.
+#L1 #L2 #H elim H -H L1 L2; normalize //
+qed.
+
 (* Basic_1: removed theorems 2: wcpr0_getl wcpr0_getl_back *)