X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Flib%2Flambda%2Fext_lambda.ma;h=e0455c204363aa8f8c9485fdd59bf28e6a8ef0de;hb=d2b59bd89f761a16a2dbc663f446b4f95c767b83;hp=a183047e0276482c2a791442e2e33bc234384fc2;hpb=f3091151495bc605ce2022e55741f6420f708d8e;p=helm.git

diff --git a/matita/matita/lib/lambda/ext_lambda.ma b/matita/matita/lib/lambda/ext_lambda.ma
index a183047e0..e0455c204 100644
--- a/matita/matita/lib/lambda/ext_lambda.ma
+++ b/matita/matita/lib/lambda/ext_lambda.ma
@@ -29,12 +29,12 @@ lemma lift_appl: ∀p,k,l,F. lift (Appl F l) p k =
 #p #k #l (elim l) -l /2/ #A #D #IHl #F >IHl //
 qed.
 *)
-
+(*
 lemma lift_rel_lt: ∀i,p,k. (S i) ≤ k → lift (Rel i) k p = Rel i.
 #i #p #k #Hik normalize >(le_to_leb_true … Hik) //
 qed.
-
-lemma lift_rel_ge: ∀i,p,k. (S i) ≰ k → lift (Rel i) k p = Rel (i+p).
+*)
+lemma lift_rel_not_le: ∀i,p,k. (S i) ≰ k → lift (Rel i) k p = Rel (i+p).
 #i #p #k #Hik normalize >(lt_to_leb_false (S i) k) /2/
 qed.