- some renaming and minor updates

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / etc / snv_preserve.etc

diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/snv_preserve.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/snv_preserve.etc
index 5185215c6ae66e02f8aac1af718b572f504c9a07..578937f4c84516861a887c849a8c5aa1365ea3b0 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/etc/snv_preserve.etc
+++ b/matita/matita/contribs/lambdadelta/basic_2/etc/snv_preserve.etc
@@ -1,9 +1,3 @@
-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-.
-
 lemma da_cprs_lpr: ∀h,g,G,L1,T1. ⦃G, L1⦄ ⊢ T1 ¡[h, g] →
                    ∀l. ⦃G, L1⦄ ⊢ T1 ▪[h, g] l →
                    ∀T2. ⦃G, L1⦄ ⊢ T1 ➡* T2 → ∀L2. ⦃G, L1⦄ ⊢ ➡ L2 → ⦃G, L2⦄ ⊢ T2 ▪[h, g] l.