still more additions and corrections for the article

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

diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_aaa.ma
index aa0c10865bfebc3f49e13d937606b7cab1028093..c7735d20c36ba9a2cc4ca89af5e5d4f557b1050b 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_aaa.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_aaa.ma
@@ -66,7 +66,7 @@ qed-.
 lemma cnv_inv_appl_pred (a) (h) (G) (L):
       ∀V,T. ⦃G,L⦄ ⊢ ⓐV.T ![yinj a,h] →
       ∃∃p,W0,U0. ⦃G,L⦄ ⊢ V ![a,h] & ⦃G,L⦄ ⊢ T ![a,h] &
-                   ⦃G,L⦄ ⊢ V ➡*[1,h] W0 & ⦃G,L⦄ ⊢ T ➡*[↓a,h] ⓛ{p}W0.U0.
+                 ⦃G,L⦄ ⊢ V ➡*[1,h] W0 & ⦃G,L⦄ ⊢ T ➡*[↓a,h] ⓛ{p}W0.U0.
 #a #h #G #L #V #T #H
 elim (cnv_inv_appl … H) -H #n #p #W #U #Ha #HV #HT #HVW #HTU
 lapply (ylt_inv_inj … Ha) -Ha #Ha