- a reinforement in a lemma on ldrop allows to prove a lemma on lsx :)

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

diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/cir_append.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/cir_append.ma
index bf68aedeeb4cacee24c26fba8411636cb68f7d99..efd097f8446d9cd27c086d72604ba0dfbec884f0 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/reduction/cir_append.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/cir_append.ma
@@ -15,20 +15,20 @@
 include "basic_2/reduction/crr_append.ma".
 include "basic_2/reduction/cir.ma".
 
-(* CONTEXT-SENSITIVE IRREDUCIBLE TERMS **************************************)
+(* IRREDUCIBLE TERMS FOR CONTEXT-SENSITIVE REDUCTION ************************)
 
 (* Advanved properties ******************************************************)
 
-lemma cir_labst_last: ∀G,L,T,W. ⦃G, L⦄ ⊢ 𝐈⦃T⦄  → ⦃G, ⋆.ⓛW @@ L⦄ ⊢ 𝐈⦃T⦄.
+lemma cir_labst_last: ∀G,L,T,W. ⦃G, L⦄ ⊢ ➡ 𝐈⦃T⦄  → ⦃G, ⋆.ⓛW @@ L⦄ ⊢ ➡ 𝐈⦃T⦄.
 /3 width=2 by crr_inv_labst_last/ qed.
 
-lemma cir_tif: ∀G,T,W. ⦃G, ⋆⦄ ⊢ 𝐈⦃T⦄ → ⦃G, ⋆.ⓛW⦄ ⊢ 𝐈⦃T⦄.
+lemma cir_tif: ∀G,T,W. ⦃G, ⋆⦄ ⊢ ➡ 𝐈⦃T⦄ → ⦃G, ⋆.ⓛW⦄ ⊢ ➡ 𝐈⦃T⦄.
 /3 width=2 by crr_inv_trr/ qed.
 
 (* Advanced inversion lemmas ************************************************)
 
-lemma cir_inv_append_sn: ∀G,L,K,T. ⦃G, K @@ L⦄ ⊢ 𝐈⦃T⦄  → ⦃G, L⦄ ⊢ 𝐈⦃T⦄.
+lemma cir_inv_append_sn: ∀G,L,K,T. ⦃G, K @@ L⦄ ⊢ ➡ 𝐈⦃T⦄  → ⦃G, L⦄ ⊢ ➡ 𝐈⦃T⦄.
 /3 width=1/ qed-.
 
-lemma cir_inv_tir: ∀G,T,W. ⦃G, ⋆.ⓛW⦄ ⊢ 𝐈⦃T⦄  → ⦃G, ⋆⦄ ⊢ 𝐈⦃T⦄.
+lemma cir_inv_tir: ∀G,T,W. ⦃G, ⋆.ⓛW⦄ ⊢ ➡ 𝐈⦃T⦄  → ⦃G, ⋆⦄ ⊢ ➡ 𝐈⦃T⦄.
 /3 width=1/ qed-.