X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fstatic_2%2Fstatic%2Fgcp_aaa.ma;h=d1dc57ece3d6f38721e9308849aa6039e6ef95e9;hp=d6424d236b77e3f6332c0562ca2b25410621c7c7;hb=f308429a0fde273605a2330efc63268b4ac36c99;hpb=87f57ddc367303c33e19c83cd8989cd561f3185b

diff --git a/matita/matita/contribs/lambdadelta/static_2/static/gcp_aaa.ma b/matita/matita/contribs/lambdadelta/static_2/static/gcp_aaa.ma
index d6424d236..d1dc57ece 100644
--- a/matita/matita/contribs/lambdadelta/static_2/static/gcp_aaa.ma
+++ b/matita/matita/contribs/lambdadelta/static_2/static/gcp_aaa.ma
@@ -22,9 +22,9 @@ include "static_2/static/lsubc_drops.ma".
 (* Basic_1: was: sc3_arity_csubc *)
 theorem acr_aaa_csubc_lifts: ∀RR,RS,RP.
                              gcp RR RS RP → gcr RR RS RP RP →
-                             ∀G,L1,T,A. ⦃G, L1⦄ ⊢ T ⁝ A → ∀b,f,L0. ⬇*[b, f] L0 ≘ L1 →
+                             ∀G,L1,T,A. ⦃G,L1⦄ ⊢ T ⁝ A → ∀b,f,L0. ⬇*[b,f] L0 ≘ L1 →
                              ∀T0. ⬆*[f] T ≘ T0 → ∀L2. G ⊢ L2 ⫃[RP] L0 →
-                             ⦃G, L2, T0⦄ ϵ[RP] 〚A〛.
+                             ⦃G,L2,T0⦄ ϵ[RP] 〚A〛.
 #RR #RS #RP #H1RP #H2RP #G #L1 #T @(fqup_wf_ind_eq (Ⓣ) … G L1 T) -G -L1 -T
 #Z #Y #X #IH #G #L1 * [ * | * [ #p ] * ]
 [ #s #HG #HL #HT #A #HA #b #f #L0 #HL01 #X0 #H0 #L2 #HL20 destruct -IH
@@ -91,11 +91,11 @@ qed.
 
 (* Basic_1: was: sc3_arity *)
 lemma acr_aaa: ∀RR,RS,RP. gcp RR RS RP → gcr RR RS RP RP →
-               ∀G,L,T,A. ⦃G, L⦄ ⊢ T ⁝ A → ⦃G, L, T⦄ ϵ[RP] 〚A〛.
+               ∀G,L,T,A. ⦃G,L⦄ ⊢ T ⁝ A → ⦃G,L,T⦄ ϵ[RP] 〚A〛.
 /3 width=9 by drops_refl, lifts_refl, acr_aaa_csubc_lifts/ qed.
 
 lemma gcr_aaa: ∀RR,RS,RP. gcp RR RS RP → gcr RR RS RP RP →
-               ∀G,L,T,A. ⦃G, L⦄ ⊢ T ⁝ A → RP G L T.
+               ∀G,L,T,A. ⦃G,L⦄ ⊢ T ⁝ A → RP G L T.
 #RR #RS #RP #H1RP #H2RP #G #L #T #A #HT
 lapply (acr_gcr … H1RP H2RP A) #HA
 @(s1 … HA) /2 width=4 by acr_aaa/