partial commit: "reduction" component

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

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 c52165e3e46d20429a3dc54a621ba482dd215fe4..7ee9e1f295bf7228a3b5e63725135c52809d598c 100644 (file)
--- 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. ⦃G, L⦄ ⊢ 𝐑⦃T⦄ → ⦃G, 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