some renaming and some typos corrected ...

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

diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/cpy_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/cpy_lift.ma
index dcc1cba83fc16583dd7bbe396bbe900c8129e346..78318917befb3801cfd6b55eb37eea554edcf100 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/substitution/cpy_lift.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/cpy_lift.ma
@@ -212,7 +212,7 @@ lemma cpy_inv_lift1_ge: ∀G,L,U1,U2,dt,et. ⦃G, L⦄ ⊢ U1 ▶[dt, et] U2 →
 ]
 qed-.
 
-(* Advancd inversion lemmas on relocation ***********************************)
+(* Advanced inversion lemmas on relocation ***********************************)
 
 lemma cpy_inv_lift1_ge_up: ∀G,L,U1,U2,dt,et. ⦃G, L⦄ ⊢ U1 ▶[dt, et] U2 →
                            ∀K,s,d,e. ⇩[s, d, e] L ≡ K → ∀T1. ⇧[d, e] T1 ≡ U1 →