still more additions and corrections for the article

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / dynamic / cnv_cpes.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpes.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpes.ma
index 190165fe69e170eae398f38e1be0c2d58a6d59b3..e0775c0211dfae85a79237c5871676a31674df55 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpes.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpes.ma
@@ -48,7 +48,7 @@ qed-.
 lemma cnv_inv_appl_pred_cpes (a) (h) (G) (L):
       ∀V,T. ⦃G,L⦄ ⊢ ⓐV.T ![yinj a,h] →
       ∃∃p,W,U. ⦃G,L⦄ ⊢ V ![a,h] & ⦃G,L⦄ ⊢ T ![a,h] &
-                 ⦃G,L⦄ ⊢ V ⬌*[h,1,0] W & ⦃G,L⦄ ⊢ T ➡*[↓a,h] ⓛ{p}W.U.
+               ⦃G,L⦄ ⊢ V ⬌*[h,1,0] W & ⦃G,L⦄ ⊢ T ➡*[↓a,h] ⓛ{p}W.U.
 #a #h #G #L #V #T #H
 elim (cnv_inv_appl_pred … H) -H #p #W #U #HV #HT #HVW #HTU
 /3 width=7 by cpms_div, ex4_3_intro/