gaxiiiiiiiiiiii

From RecordUpdate Require Export RecordSet.
Export RecordSetNotations.
From mathcomp Require Export all_ssreflect.

Set Implicit Arguments.
Unset Strict Implicit.

Variable M R : finType.

gaxiiiiiiiiiiii

Require Import Arith List.


Set Implicit Arguments.
Set Asymmetric Patterns.


Section hlist.

gaxiiiiiiiiiiii

From Autosubst Require Import Autosubst.
Require Import Ensembles.
Require Import Finite_sets.
Require Import Classical.

Set Implicit Arguments.
Unset Strict Implicit.


Notation sets := Ensemble.

gaxiiiiiiiiiiii

Require Import Ensembles.

Notation sets := Ensemble.
Notation "∅" := Empty_set.
Notation "x ∈ X" := (In _ X x)(at level 50).
Notation "A ∩ B" := (Intersection _ A B)(at level 40).
Notation "A ∪ B" := (Union _ A B)(at level 40).
Notation "A ⊂ B" := (Included _ A B)(at level 30).
Notation "A // B" := (Setminus _ A B)(at level 40).
Notation "¬ A" := (Complement _ A)(at level 40).

gaxiiiiiiiiiiii

Require Import Classical.

Set Implicit Arguments.
Unset Strict Implicit.



Inductive var := Var : nat -> var.
Inductive varp := Varp : nat -> varp.

gaxiiiiiiiiiiii

From Autosubst Require Import Autosubst.






Inductive type :=

gaxiiiiiiiiiiii

Require Import FunctionalExtensionality.


(***************)
(* Definitions *)
(***************)
(*

t := n | t.[σ] | λ t | t1 <*> t2 
σ := ids | ↑ | t ∙ σ | σ1 ∘ σ2

gaxiiiiiiiiiiii

Inductive term :=
    | One : term 
    | App : term -> term -> term
    | Abs : term -> term
    | Subst : term -> subst -> term 

with subst :=
    | ids 
    | shift
    | cons : term -> subst -> subst

gaxiiiiiiiiiiii

Require Import ZArith.

Definition var := nat.

Inductive term : Set :=
    | t_var : var -> term
    | t_abs : var -> term -> term 
    | t_app : term -> term -> term.

gaxiiiiiiiiiiii

Require Import ZArith.
Open Scope Z_scope.

Definition var := Z.

Inductive term : Set :=
    | t_var : var -> term
    | t_abs : term -> term 
    | t_app : term -> term -> term.