X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Flib%2Flambda%2Fterms.ma;h=554f8099cb453ac0719b17fb082ceddc3a2272ad;hb=e0827239f4b44f2af9c7f88c4c7c41f2a193ae37;hp=a0d262363fc9f865b88394ecf5a317a45a7fc475;hpb=f3091151495bc605ce2022e55741f6420f708d8e;p=helm.git

diff --git a/matita/matita/lib/lambda/terms.ma b/matita/matita/lib/lambda/terms.ma
index a0d262363..554f8099c 100644
--- a/matita/matita/lib/lambda/terms.ma
+++ b/matita/matita/lib/lambda/terms.ma
@@ -33,6 +33,7 @@ lemma appl_append: ∀N,l,M. Appl M (l @ [N]) = App (Appl M l) N.
 #N #l elim l -l // #hd #tl #IHl #M >IHl //
 qed.
 
+(*
 let rec is_dummy t ≝ match t with
    [ Sort _     ⇒ false
    | Rel _      ⇒ false
@@ -41,7 +42,7 @@ let rec is_dummy t ≝ match t with
    | Prod _ _   ⇒ false       (* not so sure yet *)
    | D _        ⇒ true
    ].
-
+*)
 (* nautral terms *)
 inductive neutral: T → Prop ≝
    | neutral_sort: ∀n.neutral (Sort n)