16 lines
471 B
Coq
16 lines
471 B
Coq
|
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).
|