Require Undecidability.L.L.
Require Import List.
Import L (term, var, app, lam).

Inductive sty : Type :=
  | atom : nat -> sty
  | arr : sty -> list sty -> sty -> sty.

Notation ty := (sty * list sty)%type.

Inductive type_assignment (Gamma : list ty) : term -> sty -> Prop :=
  | type_assignment_var x s phi t :
      nth_error Gamma x = Some (s, phi) ->
      In t (s::phi) ->
      type_assignment Gamma (var x) t
  | type_assignment_app M N s phi t :
      type_assignment Gamma M (arr s phi t) ->
      type_assignment Gamma N s ->
      Forall (type_assignment Gamma N) phi ->
      type_assignment Gamma (app M N) t
  | type_assignment_arr M s phi t :
      type_assignment ((s, phi) :: Gamma) M t ->
      type_assignment Gamma (lam M) (arr s phi t).

Definition CD_TC : (list ty) * term * sty -> Prop :=
  fun '(Gamma, M, t) => type_assignment Gamma M t.

Definition CD_TYP : term -> Prop :=
  fun M => exists Gamma t, type_assignment Gamma M t.

Definition CD_INH : (list ty) * sty -> Prop :=
  fun '(Gamma, t) => exists M, type_assignment Gamma M t.