- support for candidates of reducibility continues ...

[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 5c92a129312e272085f34d31a2f20e8dcd4841e9..05f698ff8fb9931a7b5357efae2252d7b4541710 100644 (file)
--- a/matita/matita/contribs/lambda_delta/Basic_2/functional/subst.ma
+++ b/matita/matita/contribs/lambda_delta/Basic_2/functional/subst.ma
@@ -20,7 +20,7 @@ include "Basic_2/functional/lift.ma".
 let rec fsubst W d U on U ≝ match U with
 [ TAtom I     ⇒ match I with
   [ Sort _ ⇒ U
-  | LRef i â\87\92 tri â\80¦ i d (#i) (â\86\9f[0, i] W) (#(i-1))
+  | LRef i â\87\92 tri â\80¦ i d (#i) (â\86\91[0, i] W) (#(i-1))
   | GRef _ ⇒ U
   ]
 | TPair I V T ⇒ match I with
@@ -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.
-                       â\86\93[0, d] L â\89¡ K. ð\9d\95\93{Abbr} V â\86\92 L â\8a¢ T [d, 1] â\89¡ â\86¡[d ← V] T.
+                       â\87\93[0, d] L â\89¡ K. ð\9d\95\93{Abbr} V â\86\92 L â\8a¢ T [d, 1] â\89¡ â\86\93[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,8 +48,8 @@ qed.
 
 (* Main inversion properties ************************************************)
 
-theorem fsubst_inv_delift: â\88\80K,V,T1,L,T2,d. â\86\93[0, d] L â\89¡ K. ð\9d\95\93{Abbr} V â\86\92
-                           L â\8a¢ T1 [d, 1] â\89¡ T2 â\86\92 â\86¡[d ← V] T1 = T2.
+theorem fsubst_inv_delift: â\88\80K,V,T1,L,T2,d. â\87\93[0, d] L â\89¡ K. ð\9d\95\93{Abbr} V â\86\92
+                           L â\8a¢ T1 [d, 1] â\89¡ T2 â\86\92 â\86\93[d ← V] T1 = T2.
 #K #V #T1 elim T1 -T1
 [ * #i #L #T2 #d #HLK #H
   [ -HLK >(delift_fwd_sort1 … H) -H //
@@ -71,4 +71,3 @@ theorem fsubst_inv_delift: ∀K,V,T1,L,T2,d. ↓[0, d] L ≡ K. 𝕓{Abbr} V →
   ]
 ]
 qed-.
- 
\ No newline at end of file