- revision of ground_2 and basic_2

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / multiple / lifts.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_2/multiple/lifts.ma b/matita/matita/contribs/lambdadelta/basic_2/multiple/lifts.ma
index be2d50f1e25d38e4f8733f239e54f98de49bbda2..7a091abced075aa2667e1a5f3a84fa1d2be8ecf6 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/multiple/lifts.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/multiple/lifts.ma
@@ -18,7 +18,7 @@ include "basic_2/multiple/mr2_plus.ma".
 
 (* GENERIC TERM RELOCATION **************************************************)
 
-inductive lifts: list2 nat nat → relation term ≝
+inductive lifts: list2 ynat nat → relation term ≝
 | lifts_nil : ∀T. lifts (◊) T T
 | lifts_cons: ∀T1,T,T2,cs,l,m.
               ⬆[l,m] T1 ≡ T → lifts cs T T2 → lifts ({l, m} @ cs) T1 T2