| App: T → T → T (* function, argument *)
| Lambda: T → T → T (* type, body *)
| Prod: T → T → T (* type, body *)
| App: T → T → T (* function, argument *)
| Lambda: T → T → T (* type, body *)
| Prod: T → T → T (* type, body *)
inductive neutral: T → Prop ≝
| neutral_sort: ∀n.neutral (Sort n)
| neutral_rel: ∀i.neutral (Rel i)
| neutral_app: ∀M,N.neutral (App M N)
inductive neutral: T → Prop ≝
| neutral_sort: ∀n.neutral (Sort n)
| neutral_rel: ∀i.neutral (Rel i)
| neutral_app: ∀M,N.neutral (App M N)