X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fdynamic%2Fcnv_aaa.ma;h=aa0c10865bfebc3f49e13d937606b7cab1028093;hp=c63a1aa1209760964af4074632213d6ba11978b8;hb=f308429a0fde273605a2330efc63268b4ac36c99;hpb=87f57ddc367303c33e19c83cd8989cd561f3185b

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 c63a1aa12..aa0c10865 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_aaa.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_aaa.ma
@@ -22,7 +22,7 @@ include "basic_2/dynamic/cnv.ma".
 (* Forward lemmas on atomic arity assignment for terms **********************)
 
 (* Basic_2A1: uses: snv_fwd_aaa *)
-lemma cnv_fwd_aaa (a) (h): ∀G,L,T. ⦃G, L⦄ ⊢ T ![a, h] → ∃A. ⦃G, L⦄ ⊢ T ⁝ A.
+lemma cnv_fwd_aaa (a) (h): ∀G,L,T. ⦃G,L⦄ ⊢ T ![a,h] → ∃A. ⦃G,L⦄ ⊢ T ⁝ A.
 #a #h #G #L #T #H elim H -G -L -T
 [ /2 width=2 by aaa_sort, ex_intro/
 | #I #G #L #V #_ * /3 width=2 by aaa_zero, ex_intro/
@@ -46,7 +46,7 @@ qed-.
 (* Forward lemmas with t_bound rt_transition for terms **********************)
 
 lemma cnv_fwd_cpm_SO (a) (h) (G) (L):
-      ∀T. ⦃G, L⦄ ⊢ T ![a, h] → ∃U. ⦃G,L⦄ ⊢ T ➡[1,h] U.
+      ∀T. ⦃G,L⦄ ⊢ T ![a,h] → ∃U. ⦃G,L⦄ ⊢ T ➡[1,h] U.
 #a #h #G #L #T #H
 elim (cnv_fwd_aaa … H) -H #A #HA
 /2 width=2 by aaa_cpm_SO/
@@ -55,7 +55,7 @@ qed-.
 (* Forward lemmas with t_bound rt_computation for terms *********************)
 
 lemma cnv_fwd_cpms_total (a) (h) (n) (G) (L):
-      ∀T. ⦃G, L⦄ ⊢ T ![a, h] → ∃U. ⦃G,L⦄ ⊢ T ➡*[n,h] U.
+      ∀T. ⦃G,L⦄ ⊢ T ![a,h] → ∃U. ⦃G,L⦄ ⊢ T ➡*[n,h] U.
 #a #h #n #G #L #T #H
 elim (cnv_fwd_aaa … H) -H #A #HA
 /2 width=2 by cpms_total_aaa/
@@ -64,9 +64,9 @@ qed-.
 (* Advanced inversion lemmas ************************************************)
 
 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.
+      ∀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.
 #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