- some renaming and minor updates

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / dynamic / snv_preserve.ma

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 1ee74e64abf32939723ba9e4ec83efa04a868231..5f76fea80a0cbce0d4e3d71e0509c1bc13e5c18f 100644 (file)
--- 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-.