inductive of dependently typed syntax

has_syntax.v

Inductive has_syntax : forall {T}, T -> Type :=
| App {A} {B : A -> Type} (f : forall a : A, B a) (x : A)
  : has_syntax f -> has_syntax x -> has_syntax (f x)
| Abs {A} {B : A -> Type} (f : forall a : A, B a)
  : (forall a : A, has_syntax (f a)) -> has_syntax f
| Forall A (B : A -> Type)
  : has_syntax A -> has_syntax B -> has_syntax (forall a : A, B a)
| O : has_syntax Datatypes.O
| S : has_syntax Datatypes.S
| tt : has_syntax Datatypes.tt
| existT : has_syntax (@existT)
| refl : has_syntax (@eq_refl)
| nat_rect : has_syntax (@Datatypes.nat_rect)
| unit_rect : has_syntax (@Datatypes.unit_rect)
| pr1 : has_syntax (@projT1)
| pr2 : has_syntax (@projT2)
| eq_rect : has_syntax (@Logic.eq_rect)
| Empty_rect : has_syntax (@Empty_set_rect)
| TYPE : has_syntax Type
| EMPTY : has_syntax Empty_set
| UNIT : has_syntax unit
| NAT : has_syntax nat
| SIGT : has_syntax (@sigT)
| EQ : has_syntax (@eq)
.