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

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 e2eca5cdf..190165fe6 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpes.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpes.ma
@@ -21,42 +21,42 @@ include "basic_2/dynamic/cnv_aaa.ma".
 
 lemma cnv_appl_cpes (a) (h) (G) (L):
       ∀n. yinj n < a →
-      ∀V. ⦃G, L⦄ ⊢ V ![a, h] → ∀T. ⦃G, L⦄ ⊢ T ![a, h] →
-      ∀W. ⦃G, L⦄ ⊢ V ⬌*[h,1,0] W →
-      ∀p,U. ⦃G, L⦄ ⊢ T ➡*[n, h] ⓛ{p}W.U → ⦃G, L⦄ ⊢ ⓐV.T ![a, h].
+      ∀V. ⦃G,L⦄ ⊢ V ![a,h] → ∀T. ⦃G,L⦄ ⊢ T ![a,h] →
+      ∀W. ⦃G,L⦄ ⊢ V ⬌*[h,1,0] W →
+      ∀p,U. ⦃G,L⦄ ⊢ T ➡*[n,h] ⓛ{p}W.U → ⦃G,L⦄ ⊢ ⓐV.T ![a,h].
 #a #h #G #L #n #Hn #V #HV #T #HT #W *
 /4 width=11 by cnv_appl, cpms_cprs_trans, cpms_bind/
 qed.
 
 lemma cnv_cast_cpes (a) (h) (G) (L):
-      ∀U. ⦃G, L⦄ ⊢ U ![a, h] →
-      ∀T. ⦃G, L⦄ ⊢ T ![a, h] → ⦃G, L⦄ ⊢ U ⬌*[h,0,1] T → ⦃G, L⦄ ⊢ ⓝU.T ![a, h].
+      ∀U. ⦃G,L⦄ ⊢ U ![a,h] →
+      ∀T. ⦃G,L⦄ ⊢ T ![a,h] → ⦃G,L⦄ ⊢ U ⬌*[h,0,1] T → ⦃G,L⦄ ⊢ ⓝU.T ![a,h].
 #a #h #G #L #U #HU #T #HT * /2 width=3 by cnv_cast/
 qed.
 
 (* Inversion lemmas with t-bound rt-equivalence for terms *******************)
 
 lemma cnv_inv_appl_cpes (a) (h) (G) (L):
-      ∀V,T. ⦃G, L⦄ ⊢ ⓐV.T ![a, h] →
-      ∃∃n,p,W,U. yinj n < a & ⦃G, L⦄ ⊢ V ![a, h] & ⦃G, L⦄ ⊢ T ![a, h] &
-                 ⦃G, L⦄ ⊢ V ⬌*[h,1,0] W & ⦃G, L⦄ ⊢ T ➡*[n, h] ⓛ{p}W.U.
+      ∀V,T. ⦃G,L⦄ ⊢ ⓐV.T ![a,h] →
+      ∃∃n,p,W,U. yinj n < a & ⦃G,L⦄ ⊢ V ![a,h] & ⦃G,L⦄ ⊢ T ![a,h] &
+                 ⦃G,L⦄ ⊢ V ⬌*[h,1,0] W & ⦃G,L⦄ ⊢ T ➡*[n,h] ⓛ{p}W.U.
 #a #h #G #L #V #T #H
 elim (cnv_inv_appl … H) -H #n #p #W #U #Hn #HV #HT #HVW #HTU
 /3 width=7 by cpms_div, ex5_4_intro/
 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.
+      ∀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.
 #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/
 qed-.
 
 lemma cnv_inv_cast_cpes (a) (h) (G) (L):
-      ∀U,T. ⦃G, L⦄ ⊢ ⓝU.T ![a, h] →
-      ∧∧ ⦃G, L⦄ ⊢ U ![a, h] & ⦃G, L⦄ ⊢ T ![a, h] & ⦃G, L⦄ ⊢ U ⬌*[h,0,1] T.
+      ∀U,T. ⦃G,L⦄ ⊢ ⓝU.T ![a,h] →
+      ∧∧ ⦃G,L⦄ ⊢ U ![a,h] & ⦃G,L⦄ ⊢ T ![a,h] & ⦃G,L⦄ ⊢ U ⬌*[h,0,1] T.
 #a #h #G #L #U #T #H
 elim (cnv_inv_cast … H) -H
 /3 width=3 by cpms_div, and3_intro/