some renaming and some typos corrected ...

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / multiple / cpys_lift.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_2/multiple/cpys_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/multiple/cpys_lift.ma
index 3e0204b825ee6ffa386a81fa79e77c9b1e225acc..d69de694e279bb1b82f7e9348b504a0e9578ac27 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/multiple/cpys_lift.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/multiple/cpys_lift.ma
@@ -44,7 +44,7 @@ lemma cpys_subst_Y2: ∀I,G,L,K,V,U1,i,d.
 @(cpys_subst … HLK … HU12) >yminus_Y_inj //
 qed.
 
-(* Advanced inverion lemmas *************************************************)
+(* Advanced inversion lemmas *************************************************)
 
 lemma cpys_inv_atom1: ∀I,G,L,T2,d,e. ⦃G, L⦄ ⊢ ⓪{I} ▶*[d, e] T2 →
                       T2 = ⓪{I} ∨