X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=matita%2Fmatita%2Fcontribs%2Flambda_delta%2Fbasic_2%2Fsubstitution%2Fldrop.ma;fp=matita%2Fmatita%2Fcontribs%2Flambda_delta%2Fbasic_2%2Fsubstitution%2Fldrop.ma;h=c93d3cd188e0bcbfd18c5a27c8594dbc2ed53cf6;hb=f79d97a42a84f94d37ad9589fcce46149ee23d12;hp=e7353d7de51287084ad7c72740714b93d926ba78;hpb=99c8b28b92ec2c44774f664f9c9ec1a458593e1d;p=helm.git

diff --git a/matita/matita/contribs/lambda_delta/basic_2/substitution/ldrop.ma b/matita/matita/contribs/lambda_delta/basic_2/substitution/ldrop.ma
index e7353d7de..c93d3cd18 100644
--- a/matita/matita/contribs/lambda_delta/basic_2/substitution/ldrop.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/substitution/ldrop.ma
@@ -215,6 +215,34 @@ lemma ldrop_lsubs_ldrop2_abbr: ∀L1,L2,d,e. L1 ≼ [d, e] L2 →
 ]
 qed.
 
+lemma dropable_sn_TC: ∀R. dropable_sn R → dropable_sn (TC … R).
+#R #HR #L1 #K1 #d #e #HLK1 #L2 #H elim H -L2
+[ #L2 #HL12
+  elim (HR … HLK1 … HL12) -HR -L1 /3 width=3/
+| #L #L2 #_ #HL2 * #K #HK1 #HLK
+  elim (HR … HLK … HL2) -HR -L /3 width=3/
+]
+qed.
+
+lemma dedropable_sn_TC: ∀R. dedropable_sn R → dedropable_sn (TC … R).
+#R #HR #L1 #K1 #d #e #HLK1 #K2 #H elim H -K2
+[ #K2 #HK12
+  elim (HR … HLK1 … HK12) -HR -K1 /3 width=3/
+| #K #K2 #_ #HK2 * #L #HL1 #HLK
+  elim (HR … HLK … HK2) -HR -K /3 width=3/
+]
+qed.
+
+lemma dropable_dx_TC: ∀R. dropable_dx R → dropable_dx (TC … R).
+#R #HR #L1 #L2 #H elim H -L2
+[ #L2 #HL12 #K2 #e #HLK2
+  elim (HR … HL12 … HLK2) -HR -L2 /3 width=3/
+| #L #L2 #_ #HL2 #IHL1 #K2 #e #HLK2
+  elim (HR … HL2 … HLK2) -HR -L2 #K #HLK #HK2
+  elim (IHL1 … HLK) -L /3 width=5/
+]
+qed.
+
 (* Basic forvard lemmas *****************************************************)
 
 (* Basic_1: was: drop_S *)