evaluation for context-sensitive extended substitution (cpye) completed!

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / substitution / cpys_alt.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/cpys_alt.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/cpys_alt.ma
index 02f2910223a5d93ec8193e01e21a9fba69b39139..6a5e2694c475e00d37276ada4ce82cdf95b182a7 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/substitution/cpys_alt.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/cpys_alt.ma
@@ -75,11 +75,13 @@ lemma cpys_cpysa: ∀G,L,T1,T2,d,e. ⦃G, L⦄ ⊢ T1 ▶*[d, e] T2 → ⦃G, L
 
 (* Basic inversion lemmas ***************************************************)
 
-lemma cpysa_cpys: ∀G,L,T1,T2,d,e. ⦃G, L⦄ ⊢ T1 ▶▶*[d, e] T2 → ⦃G, L⦄ ⊢ T1 ▶*[d, e] T2.
+lemma cpysa_inv_cpys: ∀G,L,T1,T2,d,e. ⦃G, L⦄ ⊢ T1 ▶▶*[d, e] T2 → ⦃G, L⦄ ⊢ T1 ▶*[d, e] T2.
 #G #L #T1 #T2 #d #e #H elim H -G -L -T1 -T2 -d -e
 /2 width=7 by cpys_subst, cpys_flat, cpys_bind, cpy_cpys/
 qed-.
 
+(* Advanced eliminators *****************************************************)
+
 lemma cpys_ind_alt: ∀R:ynat→ynat→relation4 genv lenv term term.
                     (∀I,G,L,d,e. R d e G L (⓪{I}) (⓪{I})) →
                     (∀I,G,L,K,V1,V2,W2,i,d,e. d ≤ yinj i → i < d + e →
@@ -96,5 +98,5 @@ lemma cpys_ind_alt: ∀R:ynat→ynat→relation4 genv lenv term term.
                     ) →
                     ∀d,e,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ▶*[d, e] T2 → R d e G L T1 T2.
 #R #H1 #H2 #H3 #H4 #d #e #G #L #T1 #T2 #H elim (cpys_cpysa … H) -G -L -T1 -T2 -d -e
-/3 width=8 by cpysa_cpys/
+/3 width=8 by cpysa_inv_cpys/
 qed-.