(* generated by Ott 0.10.17 from: common.ott common_type.ott common_typing.ott bool.ott bool_type.ott bool_typing.ott nat.ott nat_type.ott nat_typing.ott var.ott fun.ott fun_type.ott fun_typing.ott let.ott fix.ott pair.ott sum.ott record.ott variant.ott typed_misc_subst.ott *)

Require Import Arith.
Require Import Bool.
Require Import List.

Require Logic.



Definition eq_var := beq_nat.



(** syntax *)
Definition label := nat.
Definition index := nat.
Definition var := nat.

Inductive list_label_type : Set := 
 | Nil_list_label_type : list_label_type
 | Cons_list_label_type : label -> type -> list_label_type -> list_label_type
with type : Set := 
 | TyBool : type
 | TyNat : type
 | TyArrow : type -> type -> type
 | TyPair : type -> type -> type
 | TySum : type -> type -> type
 | TyRecord : list_label_type -> type
 | TyVariant : list_label_type -> type.

Inductive ctx : Set := 
 | CtxEmpty : ctx
 | CtxExtend : ctx -> var -> type -> ctx.

Inductive list_clause : Set := 
 | Nil_list_clause : list_clause
 | Cons_list_clause : clause -> list_clause -> list_clause
with list_label_term : Set := 
 | Nil_list_label_term : list_label_term
 | Cons_list_label_term : label -> term -> list_label_term -> list_label_term
with term : Set := 
 | TmTrue : term
 | TmFalse : term
 | TmIf : term -> term -> term -> term
 | TmZero : term
 | TmSucc : term -> term
 | TmPred : term -> term
 | TmIszero : term -> term
 | TmVar : var -> term
 | TmAbs : var -> type -> term -> term
 | TmApp : term -> term -> term
 | TmLet : var -> term -> term -> term
 | TmFix : term -> term
 | TmPair : term -> term -> term
 | TmProj1 : term -> term
 | TmProj2 : term -> term
 | TmInl : term -> term
 | TmInr : term -> term
 | TmCase : term -> var -> term -> var -> term -> term
 | TmRecord : list_label_term -> term
 | TmProj : term -> label -> term
 | TmTag : label -> term -> type -> term
 | TmVCase : term -> list_clause -> term
with clause : Set := 
 | ClClause : label -> var -> term -> clause.

(** auxiliary functions on the new list types *)
Fixpoint map_list_label_type (A:Set) (f:label->type->A) (l:list_label_type) {struct l} : list A :=
  match l with
  | Nil_list_label_type => nil
  | Cons_list_label_type h0 h1 tl_ => cons (f h0 h1) (map_list_label_type A f tl_)
  end.
Implicit Arguments map_list_label_type.

Fixpoint make_list_label_type (l:list (label*type)) : list_label_type :=
  match l with
  | nil  => Nil_list_label_type
  | cons (h0,h1) tl_ => Cons_list_label_type h0 h1 (make_list_label_type tl_)
  end.

Fixpoint unmake_list_label_type (l:list_label_type) :  list (label*type) :=
  match l with
  | Nil_list_label_type => nil
  | Cons_list_label_type h0 h1 tl_ =>  cons (h0,h1) (unmake_list_label_type tl_)
  end.

Fixpoint nth_list_label_type (n:nat) (l:list_label_type) {struct n} : option (label*type) :=
  match n,l with
  | 0, Cons_list_label_type h0 h1 tl_ => Some (h0,h1)
  | 0, other => None
  | S m, Nil_list_label_type => None
  | S m, Cons_list_label_type h0 h1 tl_ => nth_list_label_type m tl_
  end.
Implicit Arguments nth_list_label_type.

Fixpoint app_list_label_type (l m:list_label_type) {struct l} : list_label_type :=
  match l with
  | Nil_list_label_type => m
  | Cons_list_label_type h0 h1 tl_ => Cons_list_label_type h0 h1 (app_list_label_type tl_ m)
  end.


Fixpoint map_list_label_term (A:Set) (f:label->term->A) (l:list_label_term) {struct l} : list A :=
  match l with
  | Nil_list_label_term => nil
  | Cons_list_label_term h0 h1 tl_ => cons (f h0 h1) (map_list_label_term A f tl_)
  end.
Implicit Arguments map_list_label_term.

Fixpoint make_list_label_term (l:list (label*term)) : list_label_term :=
  match l with
  | nil  => Nil_list_label_term
  | cons (h0,h1) tl_ => Cons_list_label_term h0 h1 (make_list_label_term tl_)
  end.

Fixpoint unmake_list_label_term (l:list_label_term) :  list (label*term) :=
  match l with
  | Nil_list_label_term => nil
  | Cons_list_label_term h0 h1 tl_ =>  cons (h0,h1) (unmake_list_label_term tl_)
  end.

Fixpoint nth_list_label_term (n:nat) (l:list_label_term) {struct n} : option (label*term) :=
  match n,l with
  | 0, Cons_list_label_term h0 h1 tl_ => Some (h0,h1)
  | 0, other => None
  | S m, Nil_list_label_term => None
  | S m, Cons_list_label_term h0 h1 tl_ => nth_list_label_term m tl_
  end.
Implicit Arguments nth_list_label_term.

Fixpoint app_list_label_term (l m:list_label_term) {struct l} : list_label_term :=
  match l with
  | Nil_list_label_term => m
  | Cons_list_label_term h0 h1 tl_ => Cons_list_label_term h0 h1 (app_list_label_term tl_ m)
  end.


Fixpoint map_list_clause (A:Set) (f:clause->A) (l:list_clause) {struct l} : list A :=
  match l with
  | Nil_list_clause => nil
  | Cons_list_clause h tl_ => cons (f h) (map_list_clause A f tl_)
  end.
Implicit Arguments map_list_clause.

Fixpoint make_list_clause (l:list clause) : list_clause :=
  match l with
  | nil  => Nil_list_clause
  | cons h tl_ => Cons_list_clause h (make_list_clause tl_)
  end.

Fixpoint unmake_list_clause (l:list_clause) :  list clause :=
  match l with
  | Nil_list_clause => nil
  | Cons_list_clause h tl_ =>  cons h (unmake_list_clause tl_)
  end.

Fixpoint nth_list_clause (n:nat) (l:list_clause) {struct n} : option clause :=
  match n,l with
  | 0, Cons_list_clause h tl_ => Some h
  | 0, other => None
  | S m, Nil_list_clause => None
  | S m, Cons_list_clause h tl_ => nth_list_clause m tl_
  end.
Implicit Arguments nth_list_clause.

Fixpoint app_list_clause (l m:list_clause) {struct l} : list_clause :=
  match l with
  | Nil_list_clause => m
  | Cons_list_clause h tl_ => Cons_list_clause h (app_list_clause tl_ m)
  end.


Require Export notations.



(** We use Coq's notations so we can use the standard syntax of terms
even in Coq. However, since the syntax of the object languages is very
similar to the syntax of Coq, some confusion may easily arise. In
general, we use [true%tm] to denote an object language term
(represented as the constructor [TmTrue] in Coq) to avoid confusing it
with the ordinary boolean [true] that we use when programming directly
in Coq. **)

Delimit Scope term_scope with tm.
Bind Scope term_scope with term.



(** We use the special scope [ty_scope] for the types in our object
language. This allows us to write [Bool%ty] instead of [TyBool]. **)

Delimit Scope ty_scope with ty.
Bind Scope ty_scope with type.


Delimit Scope ctx_scope with ctx.
Bind Scope ctx_scope with ctx.

Arguments Scope CtxExtend [ctx_scope nat_scope ty_scope].


(** ** Typing contexts and variable lookup

In TAPL the typing contexts are defined informally as simple sets of
pairs of variables and types, and there is a convention that all
variables in a typing context must be distinct. In practice this means
that the same variable may not be bound twice in nested scopes.

However, including these kinds of constraints in a Coq formalization
would complicate the presentation, and the restriction is not even very
realistic: in real-world programming languages, shadowing variables
(i.e. defining a new variable with the same name as one that is already
in scope) is allowed.

So we here use a more formal definition of a typing context: a typing
context is defined by the following grammar:

G ::= empty
   |  G, x : T

So in practice it is a list of pairs of the form [x : T].

The relation [x : T in G] then means that the _rightmost_ occurrence of
[x] in the context [G] is associated with the type [T]. This allows the
same variable occur appear multiple times in the context, so we can then
type terms like [\x:Bool. \x:Nat. x].

**)


Arguments Scope TmIf [term_scope term_scope term_scope].

Notation "'true'" := (TmTrue)  : term_scope.
Notation "'false'" := (TmFalse) : term_scope.
Notation "'if' t1 'then' t2 'else' t3" := 
	 ((TmIf t1 t2 t3)) : term_scope.



Notation "'Bool'" := TyBool (at level 0, no associativity) : ty_scope.



Notation "'succ' t" := ((TmSucc t)) : term_scope.
Notation "'pred' t" := ((TmPred t)) : term_scope.
Notation "0" := (TmZero) : term_scope.
Notation "'iszero' t" := ((TmIszero t)) : term_scope.



Notation "'Nat'" := TyNat (at level 0, no associativity) : ty_scope.



Arguments Scope TmVar [nat_scope].
Arguments Scope TmAbs [_ ty_scope term_scope].
Arguments Scope TmApp [term_scope term_scope].


(** Since the stop [.] is a terminator of Coq commands, we cannot use
it as the delimiter between the binder and the body of a lambda
abstraction. We follow Coq's example and use the comma [,] here. **)

Notation "\ x : T , t" := (TmAbs x T t) : term_scope.


(** Plain juxtaposition is impossible to overload with Coq's notation
mechanism. We resort to the syntax [t1 $ t2] to express an application
of [t1] to the argument [t2]. The [$]-operator is left-associative, so
we can write [t1 $ t2 $ t3] for [(t1 $ t2) $ t3]. **)

Notation "t1 $ t2" := (TmApp t1 t2) : term_scope.


(** We represent variable _identifiers_ with plain numbers. To get an
expression representing a variable reference, we have to use the
[TmVar] constructor. In informal presentations the distinction between
a plain identifier and a variable reference is often ignored, and we
just write [x] to mean a reference to the variable named [x]. However,
since in our Coq formalization numbers and terms are different things,
we express this distinction by writing ['x] for a variable
reference. On the other hand, the identifier is unadorned when it
appears in the binding position of a lambda abstraction. Hence we
write the identity function for numbers as [\x:Nat, 'x].
**)

Notation "' n" := (TmVar n) (at level 7, no associativity) : term_scope.






Arguments Scope TyArrow [ty_scope ty_scope].
Notation "T -> U" := (TyArrow T U) : ty_scope.



Notation "'lett' x = t1 'in' t2" := ((TmLet x t1 t2)) : term_scope.



Notation "'fixx' t" := ((TmFix t)) : term_scope.



(** ** General recursion

We use the syntax [fixx t] for the fixpoint operator to avoid clashing
with the built-in [fix] keyword of Coq.

There are two evaluation rules for the fixpoint operator: the
congruence rule [E_Fix] states that as long as [t1] can be evaluated
further (i.e. it is not a value), it can be evaluated inside [fixx
t1]. This rule is not needed very often, because the usual way of
using the fixpoint operator is to give it a lambda abstraction
directly as an argument.

The computation rule [E_FixBeta] does the real work: if [t = fixx
(\x:T1.t2)], then when [t] gets evaluated, then [x] is replaced by [t]
in [t2]. Usually, [t2] is itself another lambda abstraction, which can
then refer to itself with the variable [x].

**)


Notation "{ t1 , t2 }" := ((TmPair t1 t2)) : term_scope.
Notation "t .1" := ((TmProj1 t)) : term_scope.
Notation "t .2" := ((TmProj2 t)) : term_scope.

Notation "T1 * T2" := ((TyPair T1 T2)) : ty_scope.


Notation "'inl' t1" := ((TmInl t1)) : term_scope.
Notation "'inr' t1" := ((TmInr t1)) : term_scope.
Notation "'kase' t0 'of' 'inl' x1 => t1 | 'inr' x2 => t2" :=
	 ((TmCase t0 x1 t1 x2 t2)) : term_scope.

Notation "T1 + T2" := ((TySum T1 T2)) : ty_scope.


Fixpoint subst x t' t :=
  match t with
    | (TmVar y) => if beq_nat x y then t' else t
    | (t1 $ t2)%tm => (subst x t' t1 $ subst x t' t2)%tm
    | (\ y : T , t1)%tm => if beq_nat x y then t else (\ y : T, subst x t' t1)%tm
    | (fixx t1)%tm => (fixx (subst x t' t1))%tm
    | (if t1 then t2 else t3)%tm => 
      (if (subst x t' t1) then (subst x t' t2) else (subst x t' t3))%tm
    | (succ t1)%tm => (succ (subst x t' t1))%tm
    | (pred t1)%tm => (pred (subst x t' t1))%tm
    | (iszero t1)%tm => (iszero (subst x t' t1))%tm
    | (lett y = t1 in t2)%tm => 
         (lett y = (subst x t' t1) in 
           (match beq_nat x y with Basics.true => t2 | _ => subst x t' t2 end))%tm
    | {t1, t2}%tm => {subst x t' t1, subst x t' t2}%tm
    | (t1.1)%tm => (subst x t' t1).1%tm
    | (t1.2)%tm => (subst x t' t1).2%tm
    | _ => t
  end.





(* auxiliary list types for defns *)
Inductive
list_label_var_term : Set :=
   Nil_list_label_var_term : list_label_var_term
 | Cons_list_label_var_term : label -> var -> term -> list_label_var_term -> list_label_var_term.

Fixpoint map_list_label_var_term (A:Set) (f:label->var->term->A) (l:list_label_var_term) {struct l} : list A :=
  match l with
  | Nil_list_label_var_term => nil
  | Cons_list_label_var_term h0 h1 h2 tl_ => cons (f h0 h1 h2) (map_list_label_var_term A f tl_)
  end.
Implicit Arguments map_list_label_var_term.

Fixpoint make_list_label_var_term (l:list (label*var*term)) : list_label_var_term :=
  match l with
  | nil  => Nil_list_label_var_term
  | cons (h0,h1,h2) tl_ => Cons_list_label_var_term h0 h1 h2 (make_list_label_var_term tl_)
  end.

Fixpoint unmake_list_label_var_term (l:list_label_var_term) :  list (label*var*term) :=
  match l with
  | Nil_list_label_var_term => nil
  | Cons_list_label_var_term h0 h1 h2 tl_ =>  cons (h0,h1,h2) (unmake_list_label_var_term tl_)
  end.

Fixpoint nth_list_label_var_term (n:nat) (l:list_label_var_term) {struct n} : option (label*var*term) :=
  match n,l with
  | 0, Cons_list_label_var_term h0 h1 h2 tl_ => Some (h0,h1,h2)
  | 0, other => None
  | S m, Nil_list_label_var_term => None
  | S m, Cons_list_label_var_term h0 h1 h2 tl_ => nth_list_label_var_term m tl_
  end.
Implicit Arguments nth_list_label_var_term.

Fixpoint app_list_label_var_term (l m:list_label_var_term) {struct l} : list_label_var_term :=
  match l with
  | Nil_list_label_var_term => m
  | Cons_list_label_var_term h0 h1 h2 tl_ => Cons_list_label_var_term h0 h1 h2 (app_list_label_var_term tl_ m)
  end.


Inductive
list_label : Set :=
   Nil_list_label : list_label
 | Cons_list_label : label -> list_label -> list_label.

Fixpoint map_list_label (A:Set) (f:label->A) (l:list_label) {struct l} : list A :=
  match l with
  | Nil_list_label => nil
  | Cons_list_label h tl_ => cons (f h) (map_list_label A f tl_)
  end.
Implicit Arguments map_list_label.

Fixpoint make_list_label (l:list label) : list_label :=
  match l with
  | nil  => Nil_list_label
  | cons h tl_ => Cons_list_label h (make_list_label tl_)
  end.

Fixpoint unmake_list_label (l:list_label) :  list label :=
  match l with
  | Nil_list_label => nil
  | Cons_list_label h tl_ =>  cons h (unmake_list_label tl_)
  end.

Fixpoint nth_list_label (n:nat) (l:list_label) {struct n} : option label :=
  match n,l with
  | 0, Cons_list_label h tl_ => Some h
  | 0, other => None
  | S m, Nil_list_label => None
  | S m, Cons_list_label h tl_ => nth_list_label m tl_
  end.
Implicit Arguments nth_list_label.

Fixpoint app_list_label (l m:list_label) {struct l} : list_label :=
  match l with
  | Nil_list_label => m
  | Cons_list_label h tl_ => Cons_list_label h (app_list_label tl_ m)
  end.


Inductive
list_term : Set :=
   Nil_list_term : list_term
 | Cons_list_term : term -> list_term -> list_term.

Fixpoint map_list_term (A:Set) (f:term->A) (l:list_term) {struct l} : list A :=
  match l with
  | Nil_list_term => nil
  | Cons_list_term h tl_ => cons (f h) (map_list_term A f tl_)
  end.
Implicit Arguments map_list_term.

Fixpoint make_list_term (l:list term) : list_term :=
  match l with
  | nil  => Nil_list_term
  | cons h tl_ => Cons_list_term h (make_list_term tl_)
  end.

Fixpoint unmake_list_term (l:list_term) :  list term :=
  match l with
  | Nil_list_term => nil
  | Cons_list_term h tl_ =>  cons h (unmake_list_term tl_)
  end.

Fixpoint nth_list_term (n:nat) (l:list_term) {struct n} : option term :=
  match n,l with
  | 0, Cons_list_term h tl_ => Some h
  | 0, other => None
  | S m, Nil_list_term => None
  | S m, Cons_list_term h tl_ => nth_list_term m tl_
  end.
Implicit Arguments nth_list_term.

Fixpoint app_list_term (l m:list_term) {struct l} : list_term :=
  match l with
  | Nil_list_term => m
  | Cons_list_term h tl_ => Cons_list_term h (app_list_term tl_ m)
  end.


Inductive
list_label_var_term_type : Set :=
   Nil_list_label_var_term_type : list_label_var_term_type
 | Cons_list_label_var_term_type : label -> var -> term -> type -> list_label_var_term_type -> list_label_var_term_type.

Fixpoint map_list_label_var_term_type (A:Set) (f:label->var->term->type->A) (l:list_label_var_term_type) {struct l} : list A :=
  match l with
  | Nil_list_label_var_term_type => nil
  | Cons_list_label_var_term_type h0 h1 h2 h3 tl_ => cons (f h0 h1 h2 h3) (map_list_label_var_term_type A f tl_)
  end.
Implicit Arguments map_list_label_var_term_type.

Fixpoint make_list_label_var_term_type (l:list (label*var*term*type)) : list_label_var_term_type :=
  match l with
  | nil  => Nil_list_label_var_term_type
  | cons (h0,h1,h2,h3) tl_ => Cons_list_label_var_term_type h0 h1 h2 h3 (make_list_label_var_term_type tl_)
  end.

Fixpoint unmake_list_label_var_term_type (l:list_label_var_term_type) :  list (label*var*term*type) :=
  match l with
  | Nil_list_label_var_term_type => nil
  | Cons_list_label_var_term_type h0 h1 h2 h3 tl_ =>  cons (h0,h1,h2,h3) (unmake_list_label_var_term_type tl_)
  end.

Fixpoint nth_list_label_var_term_type (n:nat) (l:list_label_var_term_type) {struct n} : option (label*var*term*type) :=
  match n,l with
  | 0, Cons_list_label_var_term_type h0 h1 h2 h3 tl_ => Some (h0,h1,h2,h3)
  | 0, other => None
  | S m, Nil_list_label_var_term_type => None
  | S m, Cons_list_label_var_term_type h0 h1 h2 h3 tl_ => nth_list_label_var_term_type m tl_
  end.
Implicit Arguments nth_list_label_var_term_type.

Fixpoint app_list_label_var_term_type (l m:list_label_var_term_type) {struct l} : list_label_var_term_type :=
  match l with
  | Nil_list_label_var_term_type => m
  | Cons_list_label_var_term_type h0 h1 h2 h3 tl_ => Cons_list_label_var_term_type h0 h1 h2 h3 (app_list_label_var_term_type tl_ m)
  end.


Inductive
list_ctx_var_type_term_type : Set :=
   Nil_list_ctx_var_type_term_type : list_ctx_var_type_term_type
 | Cons_list_ctx_var_type_term_type : ctx -> var -> type -> term -> type -> list_ctx_var_type_term_type -> list_ctx_var_type_term_type.

Fixpoint map_list_ctx_var_type_term_type (A:Set) (f:ctx->var->type->term->type->A) (l:list_ctx_var_type_term_type) {struct l} : list A :=
  match l with
  | Nil_list_ctx_var_type_term_type => nil
  | Cons_list_ctx_var_type_term_type h0 h1 h2 h3 h4 tl_ => cons (f h0 h1 h2 h3 h4) (map_list_ctx_var_type_term_type A f tl_)
  end.
Implicit Arguments map_list_ctx_var_type_term_type.

Fixpoint make_list_ctx_var_type_term_type (l:list (ctx*var*type*term*type)) : list_ctx_var_type_term_type :=
  match l with
  | nil  => Nil_list_ctx_var_type_term_type
  | cons (h0,h1,h2,h3,h4) tl_ => Cons_list_ctx_var_type_term_type h0 h1 h2 h3 h4 (make_list_ctx_var_type_term_type tl_)
  end.

Fixpoint unmake_list_ctx_var_type_term_type (l:list_ctx_var_type_term_type) :  list (ctx*var*type*term*type) :=
  match l with
  | Nil_list_ctx_var_type_term_type => nil
  | Cons_list_ctx_var_type_term_type h0 h1 h2 h3 h4 tl_ =>  cons (h0,h1,h2,h3,h4) (unmake_list_ctx_var_type_term_type tl_)
  end.

Fixpoint nth_list_ctx_var_type_term_type (n:nat) (l:list_ctx_var_type_term_type) {struct n} : option (ctx*var*type*term*type) :=
  match n,l with
  | 0, Cons_list_ctx_var_type_term_type h0 h1 h2 h3 h4 tl_ => Some (h0,h1,h2,h3,h4)
  | 0, other => None
  | S m, Nil_list_ctx_var_type_term_type => None
  | S m, Cons_list_ctx_var_type_term_type h0 h1 h2 h3 h4 tl_ => nth_list_ctx_var_type_term_type m tl_
  end.
Implicit Arguments nth_list_ctx_var_type_term_type.

Fixpoint app_list_ctx_var_type_term_type (l m:list_ctx_var_type_term_type) {struct l} : list_ctx_var_type_term_type :=
  match l with
  | Nil_list_ctx_var_type_term_type => m
  | Cons_list_ctx_var_type_term_type h0 h1 h2 h3 h4 tl_ => Cons_list_ctx_var_type_term_type h0 h1 h2 h3 h4 (app_list_ctx_var_type_term_type tl_ m)
  end.


Inductive
list_label_term_type : Set :=
   Nil_list_label_term_type : list_label_term_type
 | Cons_list_label_term_type : label -> term -> type -> list_label_term_type -> list_label_term_type.

Fixpoint map_list_label_term_type (A:Set) (f:label->term->type->A) (l:list_label_term_type) {struct l} : list A :=
  match l with
  | Nil_list_label_term_type => nil
  | Cons_list_label_term_type h0 h1 h2 tl_ => cons (f h0 h1 h2) (map_list_label_term_type A f tl_)
  end.
Implicit Arguments map_list_label_term_type.

Fixpoint make_list_label_term_type (l:list (label*term*type)) : list_label_term_type :=
  match l with
  | nil  => Nil_list_label_term_type
  | cons (h0,h1,h2) tl_ => Cons_list_label_term_type h0 h1 h2 (make_list_label_term_type tl_)
  end.

Fixpoint unmake_list_label_term_type (l:list_label_term_type) :  list (label*term*type) :=
  match l with
  | Nil_list_label_term_type => nil
  | Cons_list_label_term_type h0 h1 h2 tl_ =>  cons (h0,h1,h2) (unmake_list_label_term_type tl_)
  end.

Fixpoint nth_list_label_term_type (n:nat) (l:list_label_term_type) {struct n} : option (label*term*type) :=
  match n,l with
  | 0, Cons_list_label_term_type h0 h1 h2 tl_ => Some (h0,h1,h2)
  | 0, other => None
  | S m, Nil_list_label_term_type => None
  | S m, Cons_list_label_term_type h0 h1 h2 tl_ => nth_list_label_term_type m tl_
  end.
Implicit Arguments nth_list_label_term_type.

Fixpoint app_list_label_term_type (l m:list_label_term_type) {struct l} : list_label_term_type :=
  match l with
  | Nil_list_label_term_type => m
  | Cons_list_label_term_type h0 h1 h2 tl_ => Cons_list_label_term_type h0 h1 h2 (app_list_label_term_type tl_ m)
  end.


Inductive
list_ctx_term_type : Set :=
   Nil_list_ctx_term_type : list_ctx_term_type
 | Cons_list_ctx_term_type : ctx -> term -> type -> list_ctx_term_type -> list_ctx_term_type.

Fixpoint map_list_ctx_term_type (A:Set) (f:ctx->term->type->A) (l:list_ctx_term_type) {struct l} : list A :=
  match l with
  | Nil_list_ctx_term_type => nil
  | Cons_list_ctx_term_type h0 h1 h2 tl_ => cons (f h0 h1 h2) (map_list_ctx_term_type A f tl_)
  end.
Implicit Arguments map_list_ctx_term_type.

Fixpoint make_list_ctx_term_type (l:list (ctx*term*type)) : list_ctx_term_type :=
  match l with
  | nil  => Nil_list_ctx_term_type
  | cons (h0,h1,h2) tl_ => Cons_list_ctx_term_type h0 h1 h2 (make_list_ctx_term_type tl_)
  end.

Fixpoint unmake_list_ctx_term_type (l:list_ctx_term_type) :  list (ctx*term*type) :=
  match l with
  | Nil_list_ctx_term_type => nil
  | Cons_list_ctx_term_type h0 h1 h2 tl_ =>  cons (h0,h1,h2) (unmake_list_ctx_term_type tl_)
  end.

Fixpoint nth_list_ctx_term_type (n:nat) (l:list_ctx_term_type) {struct n} : option (ctx*term*type) :=
  match n,l with
  | 0, Cons_list_ctx_term_type h0 h1 h2 tl_ => Some (h0,h1,h2)
  | 0, other => None
  | S m, Nil_list_ctx_term_type => None
  | S m, Cons_list_ctx_term_type h0 h1 h2 tl_ => nth_list_ctx_term_type m tl_
  end.
Implicit Arguments nth_list_ctx_term_type.

Fixpoint app_list_ctx_term_type (l m:list_ctx_term_type) {struct l} : list_ctx_term_type :=
  match l with
  | Nil_list_ctx_term_type => m
  | Cons_list_ctx_term_type h0 h1 h2 tl_ => Cons_list_ctx_term_type h0 h1 h2 (app_list_ctx_term_type tl_ m)
  end.


(** definitions *)

(* defns Jtype *)
Inductive bound : var -> type -> ctx -> Prop :=    (* defn bound *)
 | B_Here : forall (x:var) (T:type) (G:ctx),
     bound x T (CtxExtend G x T)
 | B_Next : forall (x:var) (T:type) (G:ctx) (y:var) (T':type),
      (Logic.not (x = y))  ->
     bound x T G ->
     bound x T (CtxExtend G y T')
with fvs : term -> var -> Prop :=    (* defn fvs *)
 | FVS_If1 : forall (t1 t2 t3:term) (x:var),
     fvs t1 x ->
     fvs  (TmIf t1 t2 t3)  x
 | FVS_If2 : forall (t1 t2 t3:term) (x:var),
     fvs t2 x ->
     fvs  (TmIf t1 t2 t3)  x
 | FVS_If3 : forall (t1 t2 t3:term) (x:var),
     fvs t3 x ->
     fvs  (TmIf t1 t2 t3)  x
 | FVS_Var : forall (x:var),
     fvs (TmVar x) x
 | FVS_Abs : forall (y:var) (T:type) (t:term) (x:var),
      (Logic.not (x = y))  ->
     fvs t x ->
     fvs  (TmAbs y T t)  x
 | FVS_App1 : forall (t1 t2:term) (x:var),
     fvs t1 x ->
     fvs  (TmApp t1 t2)  x
 | FVS_App2 : forall (t1 t2:term) (x:var),
     fvs t2 x ->
     fvs  (TmApp t1 t2)  x
with typing : ctx -> term -> type -> Prop :=    (* defn typing *)
 | T_True : forall (G:ctx),
     typing G TmTrue TyBool
 | T_False : forall (G:ctx),
     typing G TmFalse TyBool
 | T_If : forall (G:ctx) (t1 t2 t3:term) (T:type),
     typing G t1 TyBool ->
     typing G t2 T ->
     typing G t3 T ->
     typing G (TmIf t1 t2 t3) T
 | T_Zero : forall (G:ctx),
     typing G TmZero TyNat
 | T_Succ : forall (G:ctx) (t1:term),
     typing G t1 TyNat ->
     typing G (TmSucc t1) TyNat
 | T_Pred : forall (G:ctx) (t1:term),
     typing G t1 TyNat ->
     typing G (TmPred t1) TyNat
 | T_IsZero : forall (G:ctx) (t1:term),
     typing G t1 TyNat ->
     typing G (TmIszero t1) TyBool
 | T_Var : forall (G:ctx) (x:var) (T:type),
     bound x T G ->
     typing G (TmVar x) T
 | T_Abs : forall (G:ctx) (x:var) (T1:type) (t2:term) (T2:type),
     typing (CtxExtend G x T1) t2 T2 ->
     typing G (TmAbs x T1 t2) (TyArrow T1 T2)
 | T_App : forall (G:ctx) (t1 t2:term) (T12 T11:type),
     typing G t1 (TyArrow T11 T12) ->
     typing G t2 T11 ->
     typing G (TmApp t1 t2) T12
 | T_Let : forall (G:ctx) (x:var) (t1 t2:term) (T2 T1:type),
     typing G t1 T1 ->
     typing (CtxExtend G x T1) t2 T2 ->
     typing G (TmLet x t1 t2) T2
 | T_Fix : forall (G:ctx) (t1:term) (T1:type),
     typing G t1 (TyArrow T1 T1) ->
     typing G (TmFix t1) T1
 | T_Pair : forall (G:ctx) (t1 t2:term) (T1 T2:type),
     typing G t1 T1 ->
     typing G t2 T2 ->
     typing G (TmPair t1 t2) (TyPair T1 T2)
 | T_Proj1 : forall (G:ctx) (t1:term) (T1 T2:type),
     typing G t1 (TyPair T1 T2) ->
     typing G (TmProj1 t1) T1
 | T_Proj2 : forall (G:ctx) (t1:term) (T2 T1:type),
     typing G t1 (TyPair T1 T2) ->
     typing G (TmProj2 t1) T2
 | T_Inl : forall (G:ctx) (t1:term) (T1 T2:type),
     typing G t1 T1 ->
     typing G (TmInl t1) (TySum T1 T2)
 | T_Inr : forall (G:ctx) (t1:term) (T1 T2:type),
     typing G t1 T2 ->
     typing G (TmInr t1) (TySum T1 T2)
 | T_Case : forall (G:ctx) (t0:term) (x1:var) (t1:term) (x2:var) (t2:term) (S T1 T2:type),
     typing G t0 (TySum T1 T2) ->
     typing (CtxExtend G x1 T1) t1 S ->
     typing (CtxExtend G x2 T2) t2 S ->
     typing G (TmCase t0 x1 t1 x2 t2) S
 | T_Record : forall (l_t_T_list:list_label_term_type) (G:ctx),
     (typing_list (make_list_ctx_term_type (map_list_label_term_type (fun (l_:label) (t_:term) (T_:type) => (G,t_,T_)) l_t_T_list))) ->
     typing G (TmRecord (make_list_label_term (map_list_label_term_type (fun (l_:label) (t_:term) (T_:type) => (l_,t_)) l_t_T_list))) (TyRecord (make_list_label_type (map_list_label_term_type (fun (l_:label) (t_:term) (T_:type) => (l_,T_)) l_t_T_list)))
 | T_Proj : forall (l_T_list:list_label_type) (j:index) (G:ctx) (t1:term) (t101 t102:(label*type)),
     nth_list_label_type (j - 1) l_T_list = Some t101 ->
     nth_list_label_type (j - 1) l_T_list = Some t102 ->
     typing G t1 (TyRecord l_T_list) ->
     typing G (TmProj t1 (match t102 with (l_,T_) => l_ end)) (match t101 with (l_,T_) => T_ end)
 | T_Tag : forall (l_T_list:list_label_type) (j:index) (G:ctx) (t:term) (t103 t104:(label*type)),
     nth_list_label_type (j - 1) l_T_list = Some t103 ->
     nth_list_label_type (j - 1) l_T_list = Some t104 ->
     typing G t (match t103 with (l_,T_) => T_ end) ->
     typing G (TmTag (match t104 with (l_,T_) => l_ end) t (TyVariant l_T_list)) (TyVariant l_T_list)
 | T_VCase : forall (l_x_t_T_list:list_label_var_term_type) (G:ctx) (t:term) (S:type),
     typing G t (TyVariant (make_list_label_type (map_list_label_var_term_type (fun (l_:label) (x_:var) (t_:term) (T_:type) => (l_,T_)) l_x_t_T_list))) ->
     (typing_CtxExtend_list (make_list_ctx_var_type_term_type (map_list_label_var_term_type (fun (l_:label) (x_:var) (t_:term) (T_:type) => (G,x_,T_,t_,S)) l_x_t_T_list))) ->
     typing G (TmVCase t (make_list_clause (map_list_label_var_term_type (fun (l_:label) (x_:var) (t_:term) (T_:type) => (ClClause l_ x_ t_)) l_x_t_T_list))) S
with typing_list : list_ctx_term_type -> Prop :=
 | Nil_typing_list : typing_list Nil_list_ctx_term_type
 | Cons_typing_list : forall (G:ctx) (t_:term) (T_:type) (l':list_ctx_term_type),
      ((typing G t_ T_)) -> typing_list l' ->
      typing_list (Cons_list_ctx_term_type G t_ T_ l')
with typing_CtxExtend_list : list_ctx_var_type_term_type -> Prop :=
 | Nil_typing_CtxExtend_list : typing_CtxExtend_list Nil_list_ctx_var_type_term_type
 | Cons_typing_CtxExtend_list : forall (G:ctx) (x_:var) (T_:type) (t_:term) (S:type) (l':list_ctx_var_type_term_type),
      ((typing (CtxExtend G x_ T_) t_ S)) -> typing_CtxExtend_list l' ->
      typing_CtxExtend_list (Cons_list_ctx_var_type_term_type G x_ T_ t_ S l').

(* defns Jop *)
Inductive nv : term -> Prop :=    (* defn nv *)
 | NV_Zero : 
     nv TmZero
 | NV_Succ : forall (t:term),
     nv t ->
     nv  (TmSucc t) 
with val : term -> Prop :=    (* defn val *)
 | Val_True : 
     val TmTrue
 | Val_False : 
     val TmFalse
 | Val_NV : forall (t:term),
     nv t ->
     val t
 | Val_Abs : forall (x:var) (T:type) (t:term),
     val  (TmAbs x T t) 
 | Val_Pair : forall (t1 t2:term),
     val t1 ->
     val t2 ->
     val (TmPair t1 t2)
 | Val_Inl : forall (t1:term),
     val t1 ->
     val  (TmInl t1) 
 | Val_Inr : forall (t1:term),
     val t1 ->
     val  (TmInr t1) 
 | Val_Record : forall (l_t_list:list_label_term),
     (val_list (make_list_term (map_list_label_term (fun (l_:label) (t_:term) => t_) l_t_list))) ->
     val (TmRecord l_t_list)
 | Val_Variant : forall (l:label) (t:term) (T:type),
     val t ->
     val (TmTag l t T)
with eval : term -> term -> Prop :=    (* defn eval *)
 | E_IfTrue : forall (t2 t3:term),
     eval (TmIf TmTrue t2 t3) t2
 | E_IfFalse : forall (t2 t3:term),
     eval (TmIf TmFalse t2 t3) t3
 | E_If : forall (t1 t2 t3 t1':term),
     eval t1 t1' ->
     eval (TmIf t1 t2 t3) (TmIf t1' t2 t3)
 | E_Succ : forall (t1 t1':term),
     eval t1 t1' ->
     eval (TmSucc t1) (TmSucc t1')
 | E_PredZero : 
     eval (TmPred TmZero) TmZero
 | E_PredSucc : forall (t1:term),
     nv t1 ->
     eval (TmPred  (TmSucc t1) ) t1
 | E_Pred : forall (t1 t1':term),
     eval t1 t1' ->
     eval (TmPred t1) (TmPred t1')
 | E_IsZeroZero : 
     eval (TmIszero TmZero) TmTrue
 | E_IsZeroSucc : forall (t1:term),
     nv t1 ->
     eval (TmIszero  (TmSucc t1) ) TmFalse
 | E_IsZero : forall (t1 t1':term),
     eval t1 t1' ->
     eval (TmIszero t1) (TmIszero t1')
 | E_App1 : forall (t1 t2 t1':term),
     eval t1 t1' ->
     eval (TmApp t1 t2) (TmApp t1' t2)
 | E_App2 : forall (t1 t2 t2':term),
     val t1 ->
     eval t2 t2' ->
     eval (TmApp t1 t2) (TmApp t1 t2')
 | E_AppAbs : forall (x:var) (T:type) (t12 t2:term),
     val t2 ->
     eval (TmApp  (TmAbs x T t12)  t2)  (subst  x   t2   t12 ) 
 | E_LetV : forall (x:var) (t1 t2:term),
     val t1 ->
     eval (TmLet x t1 t2)  (subst  x   t1   t2 ) 
 | E_Let : forall (x:var) (t1 t2 t1':term),
     eval t1 t1' ->
     eval (TmLet x t1 t2) (TmLet x t1' t2)
 | E_FixBeta : forall (x:var) (T1:type) (t2:term),
     eval (TmFix  (TmAbs x T1 t2) )  (subst  x    (TmFix  (TmAbs x T1 t2) )    t2 ) 
 | E_Fix : forall (t1 t1':term),
     eval t1 t1' ->
     eval (TmFix t1) (TmFix t1')
 | E_PairBeta1 : forall (t1 t2:term),
     val t1 ->
     val t2 ->
     eval (TmProj1 (TmPair t1 t2)) t1
 | E_PairBeta2 : forall (t1 t2:term),
     val t1 ->
     val t2 ->
     eval (TmProj2 (TmPair t1 t2)) t2
 | E_Proj1 : forall (t1 t1':term),
     eval t1 t1' ->
     eval (TmProj1 t1) (TmProj1 t1')
 | E_Proj2 : forall (t1 t1':term),
     eval t1 t1' ->
     eval (TmProj2 t1) (TmProj2 t1')
 | E_Pair1 : forall (t1 t2 t1':term),
     eval t1 t1' ->
     eval (TmPair t1 t2) (TmPair t1' t2)
 | E_Pair2 : forall (t1 t2 t2':term),
     val t1 ->
     eval t2 t2' ->
     eval (TmPair t1 t2) (TmPair t1 t2')
 | E_CaseInl : forall (t0:term) (x1:var) (t1:term) (x2:var) (t2:term),
     val t0 ->
     eval (TmCase (TmInl t0) x1 t1 x2 t2)  (subst  x1   t0   t1 ) 
 | E_CaseInr : forall (t0:term) (x1:var) (t1:term) (x2:var) (t2:term),
     val t0 ->
     eval (TmCase (TmInr t0) x1 t1 x2 t2)  (subst  x2   t0   t2 ) 
 | E_Case : forall (t0:term) (x1:var) (t1:term) (x2:var) (t2 t0':term),
     eval t0 t0' ->
     eval (TmCase t0 x1 t1 x2 t2) (TmCase t0' x1 t1 x2 t2)
 | E_Inl : forall (t1 t1':term),
     eval t1 t1' ->
     eval (TmInl t1) (TmInl t1')
 | E_Inr : forall (t1 t1':term),
     eval t1 t1' ->
     eval (TmInr t1) (TmInr t1')
 | E_ProjRcd : forall (l_t_list:list_label_term) (j:index) (t105 t106:(label*term)),
     nth_list_label_term (j - 1) l_t_list = Some t105 ->
     nth_list_label_term (j - 1) l_t_list = Some t106 ->
     (val_list (make_list_term (map_list_label_term (fun (l_:label) (t_:term) => t_) l_t_list))) ->
     eval (TmProj (TmRecord l_t_list) (match t106 with (l_,t_) => l_ end)) (match t105 with (l_,t_) => t_ end)
 | E_Proj : forall (t1:term) (l:label) (t1':term),
     eval t1 t1' ->
     eval (TmProj t1 l) (TmProj t1' l)
 | E_Rcd : forall (l'_list:list_label) (l_t_list:list_label_term) (j:index) (t t'm t':term) (t107 t108:(label*term)),
     nth_list_label_term (j - 1) l_t_list = Some t107 ->
     nth_list_label_term (j - 1) l_t_list = Some t108 ->
     (val_list (make_list_term (map_list_label_term (fun (l_:label) (t_:term) => t_) l_t_list))) ->
     eval t t' ->
     eval (TmRecord ((app_list_label_term l_t_list (app_list_label_term (Cons_list_label_term (match t108 with (l_,t_) => l_ end) t Nil_list_label_term) (app_list_label_term (make_list_label_term (map_list_label (fun (l'_:label) => (l'_,t'm)) l'_list)) Nil_list_label_term))))) (TmRecord ((app_list_label_term l_t_list (app_list_label_term (Cons_list_label_term (match t107 with (l_,t_) => l_ end) t' Nil_list_label_term) (app_list_label_term (make_list_label_term (map_list_label (fun (l'_:label) => (l'_,t'm)) l'_list)) Nil_list_label_term)))))
 | E_CaseVariant : forall (l_x_t_list:list_label_var_term) (j:index) (t:term) (T:type) (t109 t110 t111:(label*var*term)),
     nth_list_label_var_term (j - 1) l_x_t_list = Some t109 ->
     nth_list_label_var_term (j - 1) l_x_t_list = Some t110 ->
     nth_list_label_var_term (j - 1) l_x_t_list = Some t111 ->
     val t ->
     eval (TmVCase (TmTag (match t111 with (l_,x_,t_) => l_ end) t T) (make_list_clause (map_list_label_var_term (fun (l_:label) (x_:var) (t_:term) => (ClClause l_ x_ t_)) l_x_t_list)))  (subst  (match t110 with (l_,x_,t_) => x_ end)   t   (match t109 with (l_,x_,t_) => t_ end) ) 
 | E_VCase : forall (l_x_t_list:list_label_var_term) (t t':term),
     eval t t' ->
     eval (TmVCase t (make_list_clause (map_list_label_var_term (fun (l_:label) (x_:var) (t_:term) => (ClClause l_ x_ t_)) l_x_t_list))) (TmVCase t' (make_list_clause (map_list_label_var_term (fun (l_:label) (x_:var) (t_:term) => (ClClause l_ x_ t_)) l_x_t_list)))
 | E_Variant : forall (l1:label) (t1:term) (T:type) (t1':term),
     eval t1 t1' ->
     eval (TmTag l1 t1 T) (TmTag l1 t1' T)
with val_list : list_term -> Prop :=
 | Nil_val_list : val_list Nil_list_term
 | Cons_val_list : forall (t_:term) (l':list_term),
      ((val t_)) -> val_list l' ->
      val_list (Cons_list_term t_ l').

Notation "t1 --> t2" := (eval t1 t2) : type_scope.





Notation "{}" := CtxEmpty : ctx_scope.

Notation "{ G , x : T }" := ((CtxExtend G x T)) : ctx_scope.

Notation "|-  t : T" := (typing CtxEmpty t T) : type_scope.

Notation "G |- t : T" := (typing G t T) : type_scope.




Notation "[ x |-> t1 ] t2" :=  (subst  x   t1   t2 )  : term_scope.