- intermediate commit to allow debugging of auto tactic in xprs.ma

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

diff --git a/matita/matita/contribs/lambda_delta/apps_2/functional/subst.ma b/matita/matita/contribs/lambda_delta/apps_2/functional/subst.ma
index e8ba1c2f25e29fef1f3a509d78d7449415f7129a..8145797904b04d74e7f2514a4094ad23080667c8 100644 (file)
--- a/matita/matita/contribs/lambda_delta/apps_2/functional/subst.ma
+++ b/matita/matita/contribs/lambda_delta/apps_2/functional/subst.ma
@@ -34,12 +34,12 @@ 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. ⓓV → L ⊢ T [d, 1] ≡ [d ← V] T.
+                       ⇩[0, d] L ≡ K. ⓓV → L ⊢ ▼*[d, 1] T ≡ [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
   [ -HLK >(tri_lt ?????? Hid) /3 width=3/
-  | destruct >tri_eq /4 width=4 by tpss_strap, tps_subst, le_n, ex2_1_intro/ (**) (* too slow without trace *)   
+  | destruct >tri_eq /4 width=4 by tpss_strap2, tps_subst, le_n, ex2_1_intro/ (**) (* too slow without trace *)   
   | -HLK >(tri_gt ?????? Hid) /3 width=3/
   ]
 | * /3 width=1/ /4 width=1/
@@ -49,7 +49,7 @@ qed.
 (* Main inversion properties ************************************************)
 
 theorem fsubst_inv_delift: ∀K,V,T1,L,T2,d. ⇩[0, d] L ≡ K. ⓓV →
-                           L ⊢ T1 [d, 1] ≡ T2 → [d ← V] T1 = T2.
+                           L ⊢ ▼*[d, 1] T1 ≡ T2 → [d ← V] T1 = T2.
 #K #V #T1 elim T1 -T1
 [ * #i #L #T2 #d #HLK #H
   [ -HLK >(delift_inv_sort1 … H) -H //