X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fetc_new%2Funfold%2Funfold.etc;h=445421935a409fb143967d437c3a56a44c71aad1;hb=c3904c007394068ed823575e3be3d73a9ad92cce;hp=8ecf927a485e07dea0dae19e1732c6d7ec904403;hpb=fb246e36bb7d2731016e686e2091f6a3704bb362;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc_new/unfold/unfold.etc b/matita/matita/contribs/lambdadelta/basic_2/etc_new/unfold/unfold.etc
index 8ecf927a4..445421935 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/etc_new/unfold/unfold.etc
+++ b/matita/matita/contribs/lambdadelta/basic_2/etc_new/unfold/unfold.etc
@@ -21,7 +21,7 @@ include "basic_2/substitution/drop.ma".
 
 (* activate genv *)
 inductive unfold: relation4 genv lenv term lenv ≝
-| unfold_sort: ∀G,L,k. unfold G L (⋆k) L
+| unfold_sort: ∀G,L,s. unfold G L (⋆s) L
 | unfold_lref: ∀I,G,L1,L2,K1,K2,V,i. ⬇[i] L1 ≡ K1. ⓑ{I}V →
                unfold G K1 V K2 → ⬇[Ⓣ, |L2|, i] L2 ≡ K2 →
                unfold G L1 (#i) (L1@@L2)