- main lemmas about abstract reducibility candidates closed

[helm.git] / matita / matita / contribs / lambda_delta / Basic_2 / functional / subst.ma

diff --git a/matita/matita/contribs/lambda_delta/Basic_2/functional/subst.ma b/matita/matita/contribs/lambda_delta/Basic_2/functional/subst.ma
index d415c19d6e6c068deddabaefc8b97bd0b9980322..b12e9b413c4224ade2c06303db4157b7ef2bf679 100644 (file)
--- a/matita/matita/contribs/lambda_delta/Basic_2/functional/subst.ma
+++ b/matita/matita/contribs/lambda_delta/Basic_2/functional/subst.ma
@@ -24,8 +24,8 @@ let rec fsubst W d U on U ≝ match U with
   | GRef _ ⇒ U
   ]
 | TPair I V T ⇒ match I with
-  [ Bind I ⇒ 𝕓{I} (fsubst W d V). (fsubst W (d+1) T)
-  | Flat I ⇒ 𝕗{I} (fsubst W d V). (fsubst W d T)
+  [ Bind2 I ⇒ ⓑ{I} (fsubst W d V). (fsubst W (d+1) T)
+  | Flat2 I ⇒ ⓕ{I} (fsubst W d V). (fsubst W d T)
   ]
 ].
 
@@ -34,7 +34,7 @@ interpretation "functional core substitution" 'Subst V d T = (fsubst V d T).
 (* Main properties **********************************************************)
 
 theorem fsubst_delift: ∀K,V,T,L,d.
-                       ⇩[0, d] L ≡ K. 𝕓{Abbr} V → L ⊢ T [d, 1] ≡ [d ← V] T.
+                       ⇩[0, d] L ≡ K. ⓓV → L ⊢ T [d, 1] ≡ [d ← V] T.
 #K #V #T elim T -T
 [ * #i #L #d #HLK normalize in ⊢ (? ? ? ? ? %); /2 width=3/
   elim (lt_or_eq_or_gt i d) #Hid
@@ -48,7 +48,7 @@ qed.
 
 (* Main inversion properties ************************************************)
 
-theorem fsubst_inv_delift: ∀K,V,T1,L,T2,d. ⇩[0, d] L ≡ K. 𝕓{Abbr} V →
+theorem fsubst_inv_delift: ∀K,V,T1,L,T2,d. ⇩[0, d] L ≡ K. ⓓV →
                            L ⊢ T1 [d, 1] ≡ T2 → [d ← V] T1 = T2.
 #K #V #T1 elim T1 -T1
 [ * #i #L #T2 #d #HLK #H