#N #l elim l -l // #hd #tl #IHl #M >IHl //
qed.
+(*
let rec is_dummy t ≝ match t with
[ Sort _ ⇒ false
| Rel _ ⇒ false
| Prod _ _ ⇒ false (* not so sure yet *)
| D _ ⇒ true
].
-
+*)
(* nautral terms *)
inductive neutral: T → Prop ≝
| neutral_sort: ∀n.neutral (Sort n)