update in static_2

[helm.git] / matita / matita / contribs / lambdadelta / static_2 / static / gcp_aaa.ma

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 7fa84f9fbc09280f229c6f30b09d8992d8336930..58e3084f6854e7d95f7d95e265e47096486ee436 100644 (file)
--- a/matita/matita/contribs/lambdadelta/static_2/static/gcp_aaa.ma
+++ b/matita/matita/contribs/lambdadelta/static_2/static/gcp_aaa.ma
@@ -22,8 +22,8 @@ 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 →
-                             â\88\80G,L1,T,A. â¦\83G,L1â¦\84 â\8a¢ T â\81\9d A â\86\92 â\88\80b,f,L0. â¬\87*[b,f] L0 ≘ L1 →
-                             â\88\80T0. â¬\86*[f] T ≘ T0 → ∀L2. G ⊢ L2 ⫃[RP] L0 →
+                             â\88\80G,L1,T,A. â¦\83G,L1â¦\84 â\8a¢ T â\81\9d A â\86\92 â\88\80b,f,L0. â\87©*[b,f] L0 ≘ L1 →
+                             â\88\80T0. â\87§*[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 ] * ]