update in ground_2 and basic_2 ...

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / computation / cprs_lift.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/cprs_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/cprs_lift.ma
index ca1556a8e7f36c5afb496f9d258e180d0affba39..b883ad18e56a76a11157c1f0976c01d5db7d0c7b 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/computation/cprs_lift.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/computation/cprs_lift.ma
@@ -44,7 +44,7 @@ lemma cprs_inv_lref1: ∀G,L,T2,i. ⦃G, L⦄ ⊢ #i ➡* T2 →
 | * #K #V1 #T1 #HLK #HVT1 #HT1
   lapply (ldrop_fwd_drop2 … HLK) #H0LK
   elim (cpr_inv_lift1 … HT2 … H0LK … HT1) -H0LK -T
- /4 width=6 by cprs_strap1, ex3_3_intro, or_intror/
+  /4 width=6 by cprs_strap1, ex3_3_intro, or_intror/
 ]
 qed-.