X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambda%2Fdelifting_substitution.ma;h=79a65396abd7f2e13021d5214823538c3034ac3d;hb=30961a10d1cdfd74c4a662082419b717b85d63a6;hp=11ce887611a10fef06cf2f1cc6aa61476a89ead6;hpb=5e24c923ea53c31c3e167c4ff7851877ded646c1;p=helm.git

diff --git a/matita/matita/contribs/lambda/delifting_substitution.ma b/matita/matita/contribs/lambda/delifting_substitution.ma
index 11ce88761..79a65396a 100644
--- a/matita/matita/contribs/lambda/delifting_substitution.ma
+++ b/matita/matita/contribs/lambda/delifting_substitution.ma
@@ -143,3 +143,22 @@ qed.
 
 definition dsubstable_dx: predicate (relation term) ≝ λR.
                           ∀D,M1,M2. R M1 M2 → ∀d. R ([d ⬐ D] M1) ([d ⬐ D] M2).
+
+definition dsubstable_sn: predicate (relation term) ≝ λR.
+                          ∀D1,D2. R D1 D2 → ∀M,d. R ([d ⬐ D1] M) ([d ⬐ D2] M).
+
+definition dsubstable: predicate (relation term) ≝ λR.
+                       ∀D1,D2. R D1 D2 → ∀M1,M2. R M1 M2 → ∀d. R ([d ⬐ D1] M1) ([d ⬐ D2] M2).
+
+lemma star_dsubstable_dx: ∀R. dsubstable_dx R → dsubstable_dx (star … R).
+#R #HR #D #M1 #M2 #H elim H -M2 // /3 width=3/
+qed.
+
+lemma star_dsubstable_sn: ∀R. dsubstable_sn R → dsubstable_sn (star … R).
+#R #HR #D1 #D2 #H elim H -D2 // /3 width=3/
+qed.
+
+lemma lstar_dsubstable_dx: ∀T,R. (∀t. dsubstable_dx (R t)) →
+                           ∀l. dsubstable_dx (lstar T … R l).
+#T #R #HR #l #D #M1 #M2 #H elim H -l -M1 -M2 // /3 width=3/
+qed.