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

diff --git a/matita/matita/lib/lambda/ext_lambda.ma b/matita/matita/lib/lambda/ext_lambda.ma
index 952161107..a183047e0 100644
--- a/matita/matita/lib/lambda/ext_lambda.ma
+++ b/matita/matita/lib/lambda/ext_lambda.ma
@@ -17,19 +17,10 @@ include "lambda/subst.ma".
 
 (* MATTER CONCERNING STRONG NORMALIZATION TO BE PUT ELSEWHERE *****************)
 
-(* terms **********************************************************************)
-
-(* FG: not needed for now 
-(* nautral terms *)
-inductive neutral: T → Prop ≝
-   | neutral_sort: ∀n.neutral (Sort n)
-   | neutral_rel: ∀i.neutral (Rel i)
-   | neutral_app: ∀M,N.neutral (App M N)
-.
-*)
-
 (* substitution ***************************************************************)
-
+(*
+axiom is_dummy_lift: ∀p,t,k. is_dummy (lift t k p) = is_dummy t.
+*)
 (* FG: do we need this? 
 definition lift0 ≝ λp,k,M . lift M p k. (**) (* remove definition *)