X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Freduction%2Fcir_append.ma;h=bf68aedeeb4cacee24c26fba8411636cb68f7d99;hb=b3c3ea1c87cbd7a87c8c29a276fc16f9ebbfb5bd;hp=fb88321efa402015c907c415ef2c51f0d9230e09;hpb=ef49e0e7f5f298c299afdd3cbfdc2404ecb93879;p=helm.git

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 fb88321ef..bf68aedee 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/reduction/cir_append.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/cir_append.ma
@@ -19,16 +19,16 @@ include "basic_2/reduction/cir.ma".
 
 (* Advanved properties ******************************************************)
 
-lemma cir_labst_last: ∀L,T,W. L ⊢ 𝐈⦃T⦄  → ⋆.ⓛ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: ∀T,W. ⋆ ⊢ 𝐈⦃T⦄ → ⋆.ⓛ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: ∀L,K,T. K @@ L ⊢ 𝐈⦃T⦄  → 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: ∀T,W. ⋆.ⓛW ⊢ 𝐈⦃T⦄  → ⋆ ⊢ 𝐈⦃T⦄.
+lemma cir_inv_tir: ∀G,T,W. ⦃G, ⋆.ⓛW⦄ ⊢ 𝐈⦃T⦄  → ⦃G, ⋆⦄ ⊢ 𝐈⦃T⦄.
 /3 width=1/ qed-.