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

diff --git a/matita/matita/lib/lambda/terms.ma b/matita/matita/lib/lambda/terms.ma
index 915c13446..554f8099c 100644
--- a/matita/matita/lib/lambda/terms.ma
+++ b/matita/matita/lib/lambda/terms.ma
@@ -32,3 +32,20 @@ let rec Appl F l on l ≝ match l with
 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
+   | App M _    ⇒ is_dummy M
+   | Lambda _ M ⇒ is_dummy M
+   | Prod _ _   ⇒ false       (* not so sure yet *)
+   | D _        ⇒ true
+   ].
+*)
+(* 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)
+.