update in ground_2, static_2, basic_2, apps_2, alpha_1

[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 58e3084f6854e7d95f7d95e265e47096486ee436..9f5d13b6596a8cda5f7a23091390bab3898cbb4a 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_csubc_lifts: ∀RR,RS,RP.
                              gcp RR RS RP → gcr RR RS RP RP →
-                             â\88\80G,L1,T,A. â¦\83G,L1â¦\84 ⊢ 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 →
-                             â¦\83G,L2,T0â¦\84 ϵ[RP] ã\80\9aAã\80\9b.
+                             â\9dªG,L2,T0â\9d« ϵ â\9f¦Aâ\9f§[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
@@ -41,7 +41,7 @@ theorem acr_aaa_csubc_lifts: ∀RR,RS,RP.
   lapply (drops_tls_at … Hf … HY) -Hf -HY #HY
   elim (drops_inv_skip2 … HY) -HY #Z #K0 #HK01 #HZ #H destruct
   elim (liftsb_inv_pair_sn … HZ) -HZ #V0 #HV10 #H destruct
-  elim (lifts_total V0 (ð\9d\90\94â\9d´â\86\91jâ\9dµ)) #V #HV0
+  elim (lifts_total V0 (ð\9d\90\94â\9d¨â\86\91jâ\9d©)) #V #HV0
   elim (lsubc_drops_trans_isuni … HL20 … HLK0) -HL20 -HLK0 // #Y #HLK2 #H
   elim (lsubc_inv_bind2 … H) -H *
   [ #K2 #HK20 #H destruct
@@ -52,7 +52,7 @@ theorem acr_aaa_csubc_lifts: ∀RR,RS,RP.
     lapply (drops_isuni_fwd_drop2 … HLK2) // #HLK2b
     lapply (aaa_lifts … HKV1 … HK01 … HV10) -HKV1 -HK01 -HV10 #HKV0A
     lapply (aaa_mono … HKV0B … HKV0A) #H destruct -HKV0B -HKV0A
-    elim (lifts_total V2 (ð\9d\90\94â\9d´â\86\91jâ\9dµ)) #V3 #HV23
+    elim (lifts_total V2 (ð\9d\90\94â\9d¨â\86\91jâ\9d©)) #V3 #HV23
     lapply (s5 … HA … G … (Ⓔ) … (ⓝW2.V2) (ⓝV.V3) ????)
     [3: |*: /2 width=9 by drops_inv_gen, lifts_flat/ ] -HLK2
     lapply (s7 … HA G L2 (Ⓔ)) -HA /3 width=7 by acr_lifts/
@@ -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 →
-               â\88\80G,L,T,A. â¦\83G,Lâ¦\84 â\8a¢ T â\81\9d A â\86\92 â¦\83G,L,Tâ¦\84 ϵ[RP] ã\80\9aAã\80\9b.
+               â\88\80G,L,T,A. â\9dªG,Lâ\9d« â\8a¢ T â\81\9d A â\86\92 â\9dªG,L,Tâ\9d« ϵ â\9f¦Aâ\9f§[RP].
 /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 →
-               â\88\80G,L,T,A. â¦\83G,Lâ¦\84 ⊢ 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/