update in ground static_2 basic_2 apps_2

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

diff --git a/matita/matita/contribs/lambdadelta/static_2/static/gcp_cr.ma b/matita/matita/contribs/lambdadelta/static_2/static/gcp_cr.ma
index e1b88f5b682d1f8ce0689e7556e3cb31c4311c41..52952ea3ae6e3e24eaa2dcaa9f3b1fdd649689d3 100644 (file)
--- a/matita/matita/contribs/lambdadelta/static_2/static/gcp_cr.ma
+++ b/matita/matita/contribs/lambdadelta/static_2/static/gcp_cr.ma
@@ -28,7 +28,7 @@ definition S1 ≝ λRP,C:candidate.
 (* Note: this is Tait's iii, or Girard's CR4 *)
 definition S2 ≝ λRR:relation4 genv lenv term term. λRS:relation term. λRP,C:candidate.
                 ∀G,L,Vs. all … (RP G L) Vs →
-                â\88\80T. ð\9d\90\92â\9dªTâ\9d« → nf RR RS G L T → C G L (ⒶVs.T).
+                â\88\80T. ð\9d\90\92â\9d¨Tâ\9d© → nf RR RS G L T → C G L (ⒶVs.T).
 
 (* Note: this generalizes Tait's ii, or Girard's CR3 *)
 definition S3 ≝ λC:candidate.
@@ -148,11 +148,11 @@ lemma acr_gcr: ∀RR,RS,RP. gcp RR RS RP → gcr RR RS RP RP →
 qed.
 
 lemma acr_abst: ∀RR,RS,RP. gcp RR RS RP → gcr RR RS RP RP →
-                â\88\80p,G,L,W,T,A,B. â\9dªG,L,Wâ\9d« ϵ ⟦B⟧[RP] → (
+                â\88\80p,G,L,W,T,A,B. â\9d¨G,L,Wâ\9d© ϵ ⟦B⟧[RP] → (
                    ∀b,f,L0,V0,W0,T0. ⇩*[b,f] L0 ≘ L → ⇧*[f] W ≘ W0 → ⇧*[⫯f] T ≘ T0 →
-                                   â\9dªG,L0,V0â\9d« ϵ â\9f¦Bâ\9f§[RP] â\86\92 â\9dªG,L0,W0â\9d« ϵ â\9f¦Bâ\9f§[RP] â\86\92 â\9dªG,L0.â\93\93â\93\9dW0.V0,T0â\9d« ϵ ⟦A⟧[RP]
+                                   â\9d¨G,L0,V0â\9d© ϵ â\9f¦Bâ\9f§[RP] â\86\92 â\9d¨G,L0,W0â\9d© ϵ â\9f¦Bâ\9f§[RP] â\86\92 â\9d¨G,L0.â\93\93â\93\9dW0.V0,T0â\9d© ϵ ⟦A⟧[RP]
                 ) →
-                â\9dªG,L,â\93\9b[p]W.Tâ\9d« ϵ ⟦②B.A⟧[RP].
+                â\9d¨G,L,â\93\9b[p]W.Tâ\9d© ϵ ⟦②B.A⟧[RP].
 #RR #RS #RP #H1RP #H2RP #p #G #L #W #T #A #B #HW #HA #f #L0 #V0 #X #HL0 #H #HB
 lapply (acr_gcr … H1RP H2RP A) #HCA
 lapply (acr_gcr … H1RP H2RP B) #HCB