X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fdynamic%2Fsnv_preserve.ma;h=5f76fea80a0cbce0d4e3d71e0509c1bc13e5c18f;hb=6f1f9e20aa2775d41bba64289fc903e6612baaf3;hp=1ee74e64abf32939723ba9e4ec83efa04a868231;hpb=c2211ba58807254e75c6321cbd688db462d80fd2;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_preserve.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_preserve.ma
index 1ee74e64a..5f76fea80 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_preserve.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_preserve.ma
@@ -53,3 +53,9 @@ theorem lstas_cpr_lpr: ∀h,g,G,L,T. IH_lstas_cpr_lpr h g G L T.
 qed-.
 
 (* Advanced preservation properties *****************************************)
+
+lemma snv_cprs_lpr: ∀h,g,G,L1,T1. ⦃G, L1⦄ ⊢ T1 ¡[h, g] →
+                    ∀T2. ⦃G, L1⦄ ⊢ T1 ➡* T2 → ∀L2. ⦃G, L1⦄ ⊢ ➡ L2 → ⦃G, L2⦄ ⊢ T2 ¡[h, g].
+#h #g #G #L1 #T1 #HT1 #T2 #H
+@(cprs_ind … H) -T2 /3 width=5 by snv_cpr_lpr/
+qed-.