- main lemmas about abstract reducibility candidates closed

[helm.git] / matita / matita / contribs / lambda_delta / Basic_2 / substitution / ldrop_ldrop.ma

diff --git a/matita/matita/contribs/lambda_delta/Basic_2/substitution/ldrop_ldrop.ma b/matita/matita/contribs/lambda_delta/Basic_2/substitution/ldrop_ldrop.ma
index 2c4b8879f4d0e0db71178590f8a7ecb24bd4049c..91c0c6b705bb0a3b656b5b3f804ca7fb25b6c37e 100644 (file)
--- a/matita/matita/contribs/lambda_delta/Basic_2/substitution/ldrop_ldrop.ma
+++ b/matita/matita/contribs/lambda_delta/Basic_2/substitution/ldrop_ldrop.ma
@@ -57,9 +57,9 @@ qed.
 
 (* Basic_1: was: ldrop_conf_lt *)
 theorem ldrop_conf_lt: ∀d1,e1,L,L1. ⇩[d1, e1] L ≡ L1 →
-                       ∀e2,K2,I,V2. ⇩[0, e2] L ≡ K2. 𝕓{I} V2 →
+                       ∀e2,K2,I,V2. ⇩[0, e2] L ≡ K2. ⓑ{I} V2 →
                        e2 < d1 → let d ≝ d1 - e2 - 1 in
-                       ∃∃K1,V1. ⇩[0, e2] L1 ≡ K1. 𝕓{I} V1 &
+                       ∃∃K1,V1. ⇩[0, e2] L1 ≡ K1. ⓑ{I} V1 &
                                 ⇩[d, e1] K2 ≡ K1 & ⇧[d, e1] V1 ≡ V2.
 #d1 #e1 #L #L1 #H elim H -d1 -e1 -L -L1
 [ #d #e #e2 #K2 #I #V2 #H