From Coq Require Import Strings.String.
Require Import terms.


Inductive context : Type :=
  | ctx_assign : string -> type_term -> context -> context
  | ctx_empty : context
.

Inductive context_contains : context -> string -> type_term -> Prop :=
  | C_take : forall (x:string) (X:type_term) (Γ:context),
    (context_contains (ctx_assign x X Γ) x X)
  | C_shuffle : forall x X y Y Γ,
    (context_contains Γ x X) ->
    (context_contains (ctx_assign y Y Γ) x X).