X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fstatic%2Fgcp_aaa.ma;h=0f001a76732aa5dda8e5647c2796fde33cd639a6;hb=75f395f0febd02de8e0f881d918a8812b1425c8d;hp=21382ed90863122184cded762ef4adbbeb923a0f;hpb=d59f344b1e4b377e2f06abd9f8856d686d21b222;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/gcp_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/static/gcp_aaa.ma
index 21382ed90..0f001a767 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/static/gcp_aaa.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/static/gcp_aaa.ma
@@ -22,8 +22,8 @@ include "basic_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 →
-                             ∀T0. ⬆*[f] T ≡ T0 → ∀L2. G ⊢ L2 ⫃[RP] L0 →
+                             ∀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〛.
 #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 ] * ]