X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Freduction%2Fcnr_crr.ma;h=7ee9e1f295bf7228a3b5e63725135c52809d598c;hb=4b7a1d1c4258c10822823cb5ee1949bcdf81abcb;hp=6d68cf9e04a732b2e130c82cf2028901345edcf9;hpb=ef49e0e7f5f298c299afdd3cbfdc2404ecb93879;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/cnr_crr.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/cnr_crr.ma
index 6d68cf9e0..7ee9e1f29 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/reduction/cnr_crr.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/cnr_crr.ma
@@ -20,8 +20,8 @@ include "basic_2/reduction/cnr.ma".
 (* Advanced inversion lemmas on context-sensitive reducible terms ***********)
 
 (* Note: this property is unusual *)
-lemma cnr_inv_crr: ∀L,T. L ⊢ 𝐑⦃T⦄ → L ⊢ 𝐍⦃T⦄ → ⊥.
-#L #T #H elim H -L -T
+lemma cnr_inv_crr: ∀G,L,T. ⦃G, L⦄ ⊢ 𝐑⦃T⦄ → ⦃G, L⦄ ⊢ 𝐍⦃T⦄ → ⊥.
+#G #L #T #H elim H -L -T
 [ #L #K #V #i #HLK #H
   elim (cnr_inv_delta … HLK H)
 | #L #V #T #_ #IHV #H