X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Flib%2Flambda%2Fsubst.ma;h=ac0480224d7cc74fa39b3905ca031805efc0e07d;hb=ffbc6cd1358d61072105766052c7498a1f37c769;hp=565432a9dfb3c29231e9272df2f7cbc67e8ed55f;hpb=d7b5af5d8c6297f191cb644034b5b4cb7dfe86c1;p=helm.git

diff --git a/matita/matita/lib/lambda/subst.ma b/matita/matita/lib/lambda/subst.ma
index 565432a9d..ac0480224 100644
--- a/matita/matita/lib/lambda/subst.ma
+++ b/matita/matita/lib/lambda/subst.ma
@@ -9,16 +9,7 @@
      \ /      
       V_______________________________________________________________ *)
 
-include "arithmetics/nat.ma".
-
-inductive T : Type[0] ≝
-  | Sort: nat → T     (* starts from 0 *)
-  | Rel: nat → T      (* starts from ... ? *)
-  | App: T → T → T    (* function, argument *)
-  | Lambda: T → T → T (* type, body *)
-  | Prod: T → T → T   (* type, body *)
-  | D: T → T          (* dummifier *)
-.
+include "lambda/terms.ma".
 
 (* arguments: k is the depth (starts from 0), p is the height (starts from 0) *)
 let rec lift t k p ≝
@@ -56,10 +47,8 @@ ndefinition subst ≝ λa.λt.subst_aux t 0 a.
 notation "M [ N ]" non associative with precedence 90 for @{'Subst $N $M}.
 *)
 
-notation "M [ k := N ]" non associative with precedence 90 for @{'Subst $M $k $N}.
-
 (* interpretation "Subst" 'Subst N M = (subst N M). *)
-interpretation "Subst" 'Subst M k N = (subst M k N).
+interpretation "Subst" 'Subst1 M k N = (subst M k N).
 
 (*** properties of lift and subst ***)