- some renaming according to the written version of basic_2

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / reduction / cir_lift.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/cir_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/cir_lift.ma
index 0c518239a44b111705c14b675f6efae685faad8a..68578e5f05f3fc8d7a71c84b5ca2a31a6b42c45d 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/reduction/cir_lift.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/cir_lift.ma
@@ -15,14 +15,14 @@
 include "basic_2/reduction/crr_lift.ma".
 include "basic_2/reduction/cir.ma".
 
-(* CONTEXT-SENSITIVE IRREDUCIBLE TERMS **************************************)
+(* IRREDUCIBLE TERMS FOR CONTEXT-SENSITIVE REDUCTION ************************)
 
 (* Properties on relocation *************************************************)
 
-lemma cir_lift: ∀G,K,T. ⦃G, K⦄ ⊢ 𝐈⦃T⦄ → ∀L,s,d,e. ⇩[s, d, e] L ≡ K →
-                â\88\80U. â\87§[d, e] T â\89¡ U â\86\92 â¦\83G, Lâ¦\84 â\8a¢ 𝐈⦃U⦄.
+lemma cir_lift: ∀G,K,T. ⦃G, K⦄ ⊢ ➡ 𝐈⦃T⦄ → ∀L,s,l,m. ⬇[s, l, m] L ≡ K →
+                â\88\80U. â¬\86[l, m] T â\89¡ U â\86\92 â¦\83G, Lâ¦\84 â\8a¢ â\9e¡ 𝐈⦃U⦄.
 /3 width=8 by crr_inv_lift/ qed.
 
-lemma cir_inv_lift: ∀G,L,U. ⦃G, L⦄ ⊢ 𝐈⦃U⦄ → ∀K,s,d,e. ⇩[s, d, e] L ≡ K →
-                    â\88\80T. â\87§[d, e] T â\89¡ U â\86\92 â¦\83G, Kâ¦\84 â\8a¢ 𝐈⦃T⦄.
+lemma cir_inv_lift: ∀G,L,U. ⦃G, L⦄ ⊢ ➡ 𝐈⦃U⦄ → ∀K,s,l,m. ⬇[s, l, m] L ≡ K →
+                    â\88\80T. â¬\86[l, m] T â\89¡ U â\86\92 â¦\83G, Kâ¦\84 â\8a¢ â\9e¡ 𝐈⦃T⦄.
 /3 width=8 by crr_lift/ qed-.