X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambda%2Fdelifting_substitution.ma;h=fe45c35a297bf5b49fa22af4f6621868b2689f53;hb=2e700622e2565c6695e8c1264dd4c1207896f28c;hp=aa9d9586c65c339bf8f9102ac9fd956acd6f8d7e;hpb=5ca47b58902b9f2583ad1354b860c04ea62df46c;p=helm.git

diff --git a/matita/matita/contribs/lambda/delifting_substitution.ma b/matita/matita/contribs/lambda/delifting_substitution.ma
index aa9d9586c..fe45c35a2 100644
--- a/matita/matita/contribs/lambda/delifting_substitution.ma
+++ b/matita/matita/contribs/lambda/delifting_substitution.ma
@@ -143,23 +143,21 @@ 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
 @(lstar_ind_l ????????? H) -l -M1 // /3 width=3/
 qed.
+
+lemma star_dsubstable: ∀R. reflexive ? R →
+                       dsubstable R → dsubstable (star … R).
+#R #H1R #H2 #D1 #D2 #H elim H -D2 /3 width=1/ /3 width=5/
+qed.