- predefined_virtuals: some additions

[helm.git] / matita / matita / contribs / lambda_delta / basic_2 / computation / acp_cr.ma

diff --git a/matita/matita/contribs/lambda_delta/basic_2/computation/acp_cr.ma b/matita/matita/contribs/lambda_delta/basic_2/computation/acp_cr.ma
index 222f00da811fc09daadae3a893afcaf08786c875..5b8a2c1ea3652235976d2e5c5665d03a704ed3cb 100644 (file)
--- a/matita/matita/contribs/lambda_delta/basic_2/computation/acp_cr.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/computation/acp_cr.ma
@@ -27,7 +27,7 @@ definition S1 ≝ λRP,C:lenv→predicate term.
 (* Note: this is Tait's iii, or Girard's CR4 *)
 definition S2 ≝ λRR:lenv→relation term. λRS:relation term. λRP,C:lenv→predicate term.
                 ∀L,Vs. all … (RP L) Vs →
-                ∀T. 𝐒[T] → NF … (RR L) RS T → C L (ⒶVs.T).
+                ∀T. 𝐒⦃T⦄ → NF … (RR L) RS T → C L (ⒶVs.T).
 
 (* Note: this is Tait's ii *)
 definition S3 ≝ λRP,C:lenv→predicate term.
@@ -42,7 +42,7 @@ definition S5 ≝ λRP,C:lenv→predicate term.
                 ∀V,T. C (L. ⓓV) (ⒶV2s. T) → RP L V → C L (ⒶV1s. ⓓV. T).
 
 definition S6 ≝ λRP,C:lenv→predicate term.
-                â\88\80L,Vs,T,W. C L (â\92¶Vs. T) â\86\92 RP L W â\86\92 C L (â\92¶Vs. â\93£W. T).
+                â\88\80L,Vs,T,W. C L (â\92¶Vs. T) â\86\92 RP L W â\86\92 C L (â\92¶Vs. â\93\9dW. T).
 
 definition S7 ≝ λC:lenv→predicate term. ∀L2,L1,T1,d,e.
                 C L1 T1 → ∀T2. ⇩[d, e] L2 ≡ L1 → ⇧[d, e] T1 ≡ T2 → C L2 T2.
@@ -158,9 +158,9 @@ qed.
 lemma aacr_abst: ∀RR,RS,RP. acp RR RS RP → acr RR RS RP (λL,T. RP L T) →
                  ∀L,W,T,A,B. RP L W → (
                     ∀L0,V0,T0,des. ⇩*[des] L0 ≡ L → ⇧*[des + 1] T ≡ T0 →
-                                   ⦃L0, V0⦄ [RP] ϵ 〚B〛 → ⦃L0. ⓓV0, T0⦄ [RP] ϵ 〚A〛
+                                   ⦃L0, V0⦄ ϵ[RP] 〚B〛 → ⦃L0. ⓓV0, T0⦄ ϵ[RP] 〚A〛
                  ) →
-                 ⦃L, ⓛW. T⦄ [RP] ϵ 〚②B. A〛.
+                 ⦃L, ⓛW. T⦄ ϵ[RP] 〚②B. A〛.
 #RR #RS #RP #H1RP #H2RP #L #W #T #A #B #HW #HA #L0 #V0 #X #des #HB #HL0 #H
 lapply (aacr_acr … H1RP H2RP A) #HCA
 lapply (aacr_acr … H1RP H2RP B) #HCB