- basics: some support for abstract triangular confluence (which

[helm.git] / matita / matita / lib / lambda / ext_lambda.ma

diff --git a/matita/matita/lib/lambda/ext_lambda.ma b/matita/matita/lib/lambda/ext_lambda.ma
index 952161107dfd30fb22381076d5128fac45a2f96a..e0455c204363aa8f8c9485fdd59bf28e6a8ef0de 100644 (file)
--- 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 *)
 
@@ -38,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.