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

diff --git a/matita/matita/lib/lambda/ext_lambda.ma b/matita/matita/lib/lambda/ext_lambda.ma
deleted file mode 100644
index e0455c204..000000000
--- a/matita/matita/lib/lambda/ext_lambda.ma
+++ /dev/null
@@ -1,81 +0,0 @@
-(**************************************************************************)
-(*       ___                                                              *)
-(*      ||M||                                                             *)
-(*      ||A||       A project by Andrea Asperti                           *)
-(*      ||T||                                                             *)
-(*      ||I||       Developers:                                           *)
-(*      ||T||         The HELM team.                                      *)
-(*      ||A||         http://helm.cs.unibo.it                             *)
-(*      \   /                                                             *)
-(*       \ /        This file is distributed under the terms of the       *)
-(*        v         GNU General Public License Version 2                  *)
-(*                                                                        *)
-(**************************************************************************)
-
-include "lambda/ext.ma".
-include "lambda/subst.ma".
-
-(* MATTER CONCERNING STRONG NORMALIZATION TO BE PUT ELSEWHERE *****************)
-
-(* 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 *)
-
-lemma lift_appl: ∀p,k,l,F. lift (Appl F l) p k = 
-                             Appl (lift F p k) (map … (lift0 p k) l). 
-#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_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.
-
-lemma lift_app: ∀M,N,k,p.
-                lift (App M N) k p = App (lift M k p) (lift N k p).
-// qed.
-
-lemma lift_lambda: ∀N,M,k,p. lift (Lambda N M) k p = 
-                   Lambda (lift N k p) (lift M (k + 1) p).
-// qed.
-
-lemma lift_prod: ∀N,M,k,p.
-                 lift (Prod N M) k p = Prod (lift N k p) (lift M (k + 1) p).
-// qed.
-
-lemma subst_app: ∀M,N,k,L. (App M N)[k≝L] = App M[k≝L] N[k≝L].
-// qed.
-
-lemma subst_lambda: ∀N,M,k,L. (Lambda N M)[k≝L] = Lambda N[k≝L] M[k+1≝L].
-// qed.
-
-lemma subst_prod: ∀N,M,k,L. (Prod N M)[k≝L] = Prod N[k≝L] M[k+1≝L].
-// qed.
-
-
-axiom lift_subst_lt: ∀A,B,i,j,k. lift (B[j≝A]) (j+k) i =
-                     (lift B (j+k+1) i)[j≝lift A k i].
-
-(* telescopic delifting substitution of l in M.
- * Rel 0 is replaced with the head of l
- *)
-let rec tsubst M l on l ≝ match l with
-   [ nil      ⇒ M
-   | cons A D ⇒ (tsubst M[0≝A] D)
-   ]. 
-
-interpretation "telescopic substitution" 'Subst M l = (tsubst M l).
-
-lemma tsubst_refl: ∀l,t. (lift t 0 (|l|))[/l] = t.
-#l elim l -l; normalize // #hd #tl #IHl #t cut (S (|tl|) = |tl| + 1) // (**) (* eliminate cut *)
-qed.
-
-lemma tsubst_sort: ∀n,l. (Sort n)[/l] = Sort n.
-// qed.