additions to Basic_2

[helm.git] / matita / matita / contribs / lambda_delta / Basic_2 / substitution / ltps.ma

diff --git a/matita/matita/contribs/lambda_delta/Basic_2/substitution/ltps.ma b/matita/matita/contribs/lambda_delta/Basic_2/substitution/ltps.ma
index 9f5547ed03dcaf13ce00c3c5d59c138992beafcd..4f30025d31ce166d86fe2391364f4b0cbc9c7be5 100644 (file)
--- a/matita/matita/contribs/lambda_delta/Basic_2/substitution/ltps.ma
+++ b/matita/matita/contribs/lambda_delta/Basic_2/substitution/ltps.ma
@@ -53,6 +53,18 @@ lemma ltps_refl: ∀L,d,e. L [d, e] ▶ L.
 #L #I #V #IHL * /2 width=1/ * /2 width=1/
 qed.
 
+lemma ltps_weak_all: ∀L1,L2,d,e. L1 [d, e] ▶ L2 → L1 [0, |L2|] ▶ L2.
+#L1 #L2 #d #e #H elim H -L1 -L2 -d -e
+// /3 width=2/ /3 width=3/
+qed.
+
+(* Basic forward lemmas *****************************************************)
+
+lemma ltps_fwd_length: ∀L1,L2,d,e. L1 [d, e] ▶ L2 → |L1| = |L2|.
+#L1 #L2 #d #e #H elim H -L1 -L2 -d -e
+normalize //
+qed-.
+
 (* Basic inversion lemmas ***************************************************)
 
 fact ltps_inv_refl_O2_aux: ∀d,e,L1,L2. L1 [d, e] ▶ L2 → e = 0 → L1 = L2.
@@ -167,9 +179,9 @@ lemma ltps_inv_tps12: ∀L1,K2,I,V2,d,e. L1 [d, e] ▶ K2. ⓑ{I} V2 → 0 < d 
 /2 width=3/ qed-.
 
 (* Basic_1: removed theorems 27:
-            csubst0_clear_O csubst0_ldrop_lt csubst0_ldrop_gt csubst0_ldrop_eq
+            csubst0_clear_O csubst0_drop_lt csubst0_drop_gt csubst0_drop_eq
             csubst0_clear_O_back csubst0_clear_S csubst0_clear_trans
-            csubst0_ldrop_gt_back csubst0_ldrop_eq_back csubst0_ldrop_lt_back
+            csubst0_drop_gt_back csubst0_drop_eq_back csubst0_drop_lt_back
             csubst0_gen_sort csubst0_gen_head csubst0_getl_ge csubst0_getl_lt
             csubst0_gen_S_bind_2 csubst0_getl_ge_back csubst0_getl_lt_back
             csubst0_snd_bind csubst0_fst_bind csubst0_both_bind