update in ground static_2 basic_2 apps_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 40e757ad62b4c9bd4445c6e82a1cfd5b492ace06..046343a068b20b677f1b4a2b36861ee26a89faf4 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,9 +22,9 @@ include "static_2/static/lsubc_drops.ma".
 (* Basic_1: was: sc3_arity_csubc *)
 theorem acr_aaa_lsubc_lifts (RR) (RS) (RP):
         gcp RR RS RP → gcr RR RS RP RP →
-        â\88\80G,L1,T,A. â\9dªG,L1â\9d« ⊢ T ⁝ A → ∀b,f,L0. ⇩*[b,f] L0 ≘ L1 →
+        â\88\80G,L1,T,A. â\9d¨G,L1â\9d© ⊢ T ⁝ A → ∀b,f,L0. ⇩*[b,f] L0 ≘ L1 →
         ∀T0. ⇧*[f] T ≘ T0 → ∀L2. G ⊢ L2 ⫃[RP] L0 →
-        â\9dªG,L2,T0â\9d« ϵ ⟦A⟧[RP].
+        â\9d¨G,L2,T0â\9d© ϵ ⟦A⟧[RP].
 #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
@@ -92,12 +92,12 @@ qed.
 (* Basic_1: was: sc3_arity *)
 lemma acr_aaa (RR) (RS) (RP):
       gcp RR RS RP → gcr RR RS RP RP →
-      â\88\80G,L,T,A. â\9dªG,Lâ\9d« â\8a¢ T â\81\9d A â\86\92 â\9dªG,L,Tâ\9d« ϵ ⟦A⟧[RP].
+      â\88\80G,L,T,A. â\9d¨G,Lâ\9d© â\8a¢ T â\81\9d A â\86\92 â\9d¨G,L,Tâ\9d© ϵ ⟦A⟧[RP].
 /3 width=9 by drops_refl, lifts_refl, acr_aaa_lsubc_lifts/ qed.
 
 lemma gcr_aaa (RR) (RS) (RP):
       gcp RR RS RP → gcr RR RS RP RP →
-      â\88\80G,L,T,A. â\9dªG,Lâ\9d« ⊢ T ⁝ A → RP G L T.
+      â\88\80G,L,T,A. â\9d¨G,Lâ\9d© ⊢ 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/