Definitions

Require Import Bool.
Require Import Metalib.Metatheory.
Require Import List.
Require Import Ott.ott_list_core.
syntax
Definition ivar : Set := var. Definition constant : Set := nat. Definition blamelabel : Set := nat.
Inductive typ : Set :=
 | typ_def (D:dtyp)
 | typ_null (D:dtyp)
with dtyp : Set :=
 | dtyp_base : dtyp
 | dtyp_arrow (A:typ) (B:typ) .

Inductive label : Set :=
 | label_name (bl:blamelabel)
 | label_not_label (bl:blamelabel) .

Inductive ityp : Set :=
 | ityp_base : ityp
 | ityp_arrow (iA:ityp) (iB:ityp) .

Inductive trm : Set :=
 | t_var_b (_:nat)
 | t_var_f (x:var)
 | t_const (c:constant)
 | t_binop (M:trm) (N:trm)
 | t_abs (A:typ) (N:trm)
 | t_app (L:trm) (M:trm)
 | t_null : trm
 | t_lift (M:trm)
 | t_case (L:trm) (M:trm) (N:trm)
 | t_cast (M:trm) (A:typ) (p:label) (B:typ)
 | t_blame (p:label) .

Inductive itrm : Set :=
 | itrm_var_b (_:nat)
 | itrm_var_f (ix:ivar)
 | itrm_const (c:constant)
 | itrm_binop (iM:itrm) (iN:itrm)
 | itrm_abs (iA:ityp) (iN:itrm)
 | itrm_app (iL:itrm) (iM:itrm)
 | itrm_null : itrm .

Inductive ctrm : Set :=
 | ctrm_hole : ctrm
 | ctrm_binop_left (CM:ctrm) (N:trm)
 | ctrm_binop_right (M:trm) (CN:ctrm)
 | ctrm_abs (A:typ) (CN:ctrm)
 | ctrm_app_left (CL:ctrm) (M:trm)
 | ctrm_app_right (L:trm) (CM:ctrm)
 | ctrm_lift (CM:ctrm)
 | ctrm_case_scrutinee (CL:ctrm) (M:trm) (N:trm)
 | ctrm_case_null (L:trm) (CM:ctrm) (N:trm)
 | ctrm_case_nonnull (L:trm) (M:trm) (CN:ctrm)
 | ctrm_cast (CM:ctrm) (A:typ) (p:label) (B:typ) .

Inductive ictrm : Set :=
 | ictrm_hole : ictrm
 | ictrm_binop_left (iCM:ictrm) (iN:itrm)
 | ictrm_binop_right (iM:itrm) (iCN:ictrm)
 | ictrm_abs (iA:ityp) (iCN:ictrm)
 | ictrm_app_left (iCL:ictrm) (iM:itrm)
 | ictrm_app_right (iL:itrm) (iCM:ictrm) .

Definition ictx : Set := list ( atom × ityp ).

Definition ctx : Set := list ( atom × typ ).

auxiliary functions on the new list types library functions subrules
Definition is_adtyp_of_dtyp (D5:dtyp) : bool :=
  match D5 with
  | dtyp_basefalse
  | (dtyp_arrow A B) ⇒ (true)
end.

Definition is_atyp_of_typ (A5:typ) : bool :=
  match A5 with
  | (typ_def D) ⇒ ((is_adtyp_of_dtyp D))
  | (typ_null D) ⇒ false
end.

Fixpoint is_val_of_trm (L5:trm) : bool :=
  match L5 with
  | (t_var_b nat) ⇒ false
  | (t_var_f x) ⇒ false
  | (t_const c) ⇒ (true)
  | (t_binop M N) ⇒ false
  | (t_abs A N) ⇒ (true)
  | (t_app L M) ⇒ false
  | t_null ⇒ (true)
  | (t_lift M) ⇒ ((is_val_of_trm M))
  | (t_case L M N) ⇒ false
  | (t_cast M A p B) ⇒ ((is_val_of_trm M) && (is_atyp_of_typ A) && (is_atyp_of_typ B))
  | (t_blame p) ⇒ false
end.

arities opening up abstractions
Fixpoint open_itrm_wrt_itrm_rec (k:nat) (iL5:itrm) (iL_6:itrm) {struct iL_6}: itrm :=
  match iL_6 with
  | (itrm_var_b nat) ⇒
      match lt_eq_lt_dec nat k with
        | inleft (left _) ⇒ itrm_var_b nat
        | inleft (right _) ⇒ iL5
        | inright _itrm_var_b (nat - 1)
      end
  | (itrm_var_f ix) ⇒ itrm_var_f ix
  | (itrm_const c) ⇒ itrm_const c
  | (itrm_binop iM iN) ⇒ itrm_binop (open_itrm_wrt_itrm_rec k iL5 iM) (open_itrm_wrt_itrm_rec k iL5 iN)
  | (itrm_abs iA iN) ⇒ itrm_abs iA (open_itrm_wrt_itrm_rec (S k) iL5 iN)
  | (itrm_app iL iM) ⇒ itrm_app (open_itrm_wrt_itrm_rec k iL5 iL) (open_itrm_wrt_itrm_rec k iL5 iM)
  | itrm_nullitrm_null
end.

Fixpoint open_trm_wrt_trm_rec (k:nat) (L5:trm) (L_6:trm) {struct L_6}: trm :=
  match L_6 with
  | (t_var_b nat) ⇒
      match lt_eq_lt_dec nat k with
        | inleft (left _) ⇒ t_var_b nat
        | inleft (right _) ⇒ L5
        | inright _t_var_b (nat - 1)
      end
  | (t_var_f x) ⇒ t_var_f x
  | (t_const c) ⇒ t_const c
  | (t_binop M N) ⇒ t_binop (open_trm_wrt_trm_rec k L5 M) (open_trm_wrt_trm_rec k L5 N)
  | (t_abs A N) ⇒ t_abs A (open_trm_wrt_trm_rec (S k) L5 N)
  | (t_app L M) ⇒ t_app (open_trm_wrt_trm_rec k L5 L) (open_trm_wrt_trm_rec k L5 M)
  | t_nullt_null
  | (t_lift M) ⇒ t_lift (open_trm_wrt_trm_rec k L5 M)
  | (t_case L M N) ⇒ t_case (open_trm_wrt_trm_rec k L5 L) (open_trm_wrt_trm_rec k L5 M) (open_trm_wrt_trm_rec (S k) L5 N)
  | (t_cast M A p B) ⇒ t_cast (open_trm_wrt_trm_rec k L5 M) A p B
  | (t_blame p) ⇒ t_blame p
end.

Fixpoint open_ictrm_wrt_itrm_rec (k:nat) (iL5:itrm) (iCL5:ictrm) {struct iCL5}: ictrm :=
  match iCL5 with
  | ictrm_holeictrm_hole
  | (ictrm_binop_left iCM iN) ⇒ ictrm_binop_left (open_ictrm_wrt_itrm_rec k iL5 iCM) (open_itrm_wrt_itrm_rec k iL5 iN)
  | (ictrm_binop_right iM iCN) ⇒ ictrm_binop_right (open_itrm_wrt_itrm_rec k iL5 iM) (open_ictrm_wrt_itrm_rec k iL5 iCN)
  | (ictrm_abs iA iCN) ⇒ ictrm_abs iA (open_ictrm_wrt_itrm_rec (S k) iL5 iCN)
  | (ictrm_app_left iCL iM) ⇒ ictrm_app_left (open_ictrm_wrt_itrm_rec k iL5 iCL) (open_itrm_wrt_itrm_rec k iL5 iM)
  | (ictrm_app_right iL iCM) ⇒ ictrm_app_right (open_itrm_wrt_itrm_rec k iL5 iL) (open_ictrm_wrt_itrm_rec k iL5 iCM)
end.

Fixpoint open_ctrm_wrt_trm_rec (k:nat) (L5:trm) (CL5:ctrm) {struct CL5}: ctrm :=
  match CL5 with
  | ctrm_holectrm_hole
  | (ctrm_binop_left CM N) ⇒ ctrm_binop_left (open_ctrm_wrt_trm_rec k L5 CM) (open_trm_wrt_trm_rec k L5 N)
  | (ctrm_binop_right M CN) ⇒ ctrm_binop_right (open_trm_wrt_trm_rec k L5 M) (open_ctrm_wrt_trm_rec k L5 CN)
  | (ctrm_abs A CN) ⇒ ctrm_abs A (open_ctrm_wrt_trm_rec (S k) L5 CN)
  | (ctrm_app_left CL M) ⇒ ctrm_app_left (open_ctrm_wrt_trm_rec k L5 CL) (open_trm_wrt_trm_rec k L5 M)
  | (ctrm_app_right L CM) ⇒ ctrm_app_right (open_trm_wrt_trm_rec k L5 L) (open_ctrm_wrt_trm_rec k L5 CM)
  | (ctrm_lift CM) ⇒ ctrm_lift (open_ctrm_wrt_trm_rec k L5 CM)
  | (ctrm_case_scrutinee CL M N) ⇒ ctrm_case_scrutinee (open_ctrm_wrt_trm_rec k L5 CL) (open_trm_wrt_trm_rec k L5 M) (open_trm_wrt_trm_rec (S k) L5 N)
  | (ctrm_case_null L CM N) ⇒ ctrm_case_null (open_trm_wrt_trm_rec k L5 L) (open_ctrm_wrt_trm_rec k L5 CM) (open_trm_wrt_trm_rec (S k) L5 N)
  | (ctrm_case_nonnull L M CN) ⇒ ctrm_case_nonnull (open_trm_wrt_trm_rec k L5 L) (open_trm_wrt_trm_rec k L5 M) (open_ctrm_wrt_trm_rec (S k) L5 CN)
  | (ctrm_cast CM A p B) ⇒ ctrm_cast (open_ctrm_wrt_trm_rec k L5 CM) A p B
end.

Definition open_ictrm_wrt_itrm iL5 iCL5 := open_ictrm_wrt_itrm_rec 0 iCL5 iL5.

Definition open_ctrm_wrt_trm L5 CL5 := open_ctrm_wrt_trm_rec 0 CL5 L5.

Definition open_itrm_wrt_itrm iL5 iL_6 := open_itrm_wrt_itrm_rec 0 iL_6 iL5.

Definition open_trm_wrt_trm L5 L_6 := open_trm_wrt_trm_rec 0 L_6 L5.

terms are locally-closed pre-terms definitions

Inductive lc_trm : trm Prop :=
 | lc_t_var_f : (x:var),
     (lc_trm (t_var_f x))
 | lc_t_const : (c:constant),
     (lc_trm (t_const c))
 | lc_t_binop : (M N:trm),
     (lc_trm M)
     (lc_trm N)
     (lc_trm (t_binop M N))
 | lc_t_abs : (A:typ) (N:trm),
      ( x , lc_trm ( open_trm_wrt_trm N (t_var_f x) ) )
     (lc_trm (t_abs A N))
 | lc_t_app : (L M:trm),
     (lc_trm L)
     (lc_trm M)
     (lc_trm (t_app L M))
 | lc_t_null :
     (lc_trm t_null)
 | lc_t_lift : (M:trm),
     (lc_trm M)
     (lc_trm (t_lift M))
 | lc_t_case : (L M N:trm),
     (lc_trm L)
     (lc_trm M)
      ( x , lc_trm ( open_trm_wrt_trm N (t_var_f x) ) )
     (lc_trm (t_case L M N))
 | lc_t_cast : (M:trm) (A:typ) (p:label) (B:typ),
     (lc_trm M)
     (lc_trm (t_cast M A p B))
 | lc_t_blame : (p:label),
     (lc_trm (t_blame p)).

Inductive lc_itrm : itrm Prop :=
 | lc_itrm_var_f : (ix:ivar),
     (lc_itrm (itrm_var_f ix))
 | lc_itrm_const : (c:constant),
     (lc_itrm (itrm_const c))
 | lc_itrm_binop : (iM iN:itrm),
     (lc_itrm iM)
     (lc_itrm iN)
     (lc_itrm (itrm_binop iM iN))
 | lc_itrm_abs : (iA:ityp) (iN:itrm),
      ( ix , lc_itrm ( open_itrm_wrt_itrm iN (itrm_var_f ix) ) )
     (lc_itrm (itrm_abs iA iN))
 | lc_itrm_app : (iL iM:itrm),
     (lc_itrm iL)
     (lc_itrm iM)
     (lc_itrm (itrm_app iL iM))
 | lc_itrm_null :
     (lc_itrm itrm_null).

Inductive lc_ctrm : ctrm Prop :=
 | lc_ctrm_hole :
     (lc_ctrm ctrm_hole)
 | lc_ctrm_binop_left : (CM:ctrm) (N:trm),
     (lc_ctrm CM)
     (lc_trm N)
     (lc_ctrm (ctrm_binop_left CM N))
 | lc_ctrm_binop_right : (M:trm) (CN:ctrm),
     (lc_trm M)
     (lc_ctrm CN)
     (lc_ctrm (ctrm_binop_right M CN))
 | lc_ctrm_abs : (A:typ) (CN:ctrm),
      ( x , lc_ctrm ( open_ctrm_wrt_trm CN (t_var_f x) ) )
     (lc_ctrm (ctrm_abs A CN))
 | lc_ctrm_app_left : (CL:ctrm) (M:trm),
     (lc_ctrm CL)
     (lc_trm M)
     (lc_ctrm (ctrm_app_left CL M))
 | lc_ctrm_app_right : (L:trm) (CM:ctrm),
     (lc_trm L)
     (lc_ctrm CM)
     (lc_ctrm (ctrm_app_right L CM))
 | lc_ctrm_lift : (CM:ctrm),
     (lc_ctrm CM)
     (lc_ctrm (ctrm_lift CM))
 | lc_ctrm_case_scrutinee : (CL:ctrm) (M N:trm),
     (lc_ctrm CL)
     (lc_trm M)
      ( x , lc_trm ( open_trm_wrt_trm N (t_var_f x) ) )
     (lc_ctrm (ctrm_case_scrutinee CL M N))
 | lc_ctrm_case_null : (L:trm) (CM:ctrm) (N:trm),
     (lc_trm L)
     (lc_ctrm CM)
      ( x , lc_trm ( open_trm_wrt_trm N (t_var_f x) ) )
     (lc_ctrm (ctrm_case_null L CM N))
 | lc_ctrm_case_nonnull : (L M:trm) (CN:ctrm),
     (lc_trm L)
     (lc_trm M)
      ( x , lc_ctrm ( open_ctrm_wrt_trm CN (t_var_f x) ) )
     (lc_ctrm (ctrm_case_nonnull L M CN))
 | lc_ctrm_cast : (CM:ctrm) (A:typ) (p:label) (B:typ),
     (lc_ctrm CM)
     (lc_ctrm (ctrm_cast CM A p B)).

Inductive lc_ictrm : ictrm Prop :=
 | lc_ictrm_hole :
     (lc_ictrm ictrm_hole)
 | lc_ictrm_binop_left : (iCM:ictrm) (iN:itrm),
     (lc_ictrm iCM)
     (lc_itrm iN)
     (lc_ictrm (ictrm_binop_left iCM iN))
 | lc_ictrm_binop_right : (iM:itrm) (iCN:ictrm),
     (lc_itrm iM)
     (lc_ictrm iCN)
     (lc_ictrm (ictrm_binop_right iM iCN))
 | lc_ictrm_abs : (iA:ityp) (iCN:ictrm),
      ( ix , lc_ictrm ( open_ictrm_wrt_itrm iCN (itrm_var_f ix) ) )
     (lc_ictrm (ictrm_abs iA iCN))
 | lc_ictrm_app_left : (iCL:ictrm) (iM:itrm),
     (lc_ictrm iCL)
     (lc_itrm iM)
     (lc_ictrm (ictrm_app_left iCL iM))
 | lc_ictrm_app_right : (iL:itrm) (iCM:ictrm),
     (lc_itrm iL)
     (lc_ictrm iCM)
     (lc_ictrm (ictrm_app_right iL iCM)).
free variables
Fixpoint fv_itrm (iL5:itrm) : vars :=
  match iL5 with
  | (itrm_var_b nat) ⇒ {}
  | (itrm_var_f ix) ⇒ {{ix}}
  | (itrm_const c) ⇒ {}
  | (itrm_binop iM iN) ⇒ (fv_itrm iM) \u (fv_itrm iN)
  | (itrm_abs iA iN) ⇒ (fv_itrm iN)
  | (itrm_app iL iM) ⇒ (fv_itrm iL) \u (fv_itrm iM)
  | itrm_null{}
end.

Fixpoint fv_trm (L5:trm) : vars :=
  match L5 with
  | (t_var_b nat) ⇒ {}
  | (t_var_f x) ⇒ {{x}}
  | (t_const c) ⇒ {}
  | (t_binop M N) ⇒ (fv_trm M) \u (fv_trm N)
  | (t_abs A N) ⇒ (fv_trm N)
  | (t_app L M) ⇒ (fv_trm L) \u (fv_trm M)
  | t_null{}
  | (t_lift M) ⇒ (fv_trm M)
  | (t_case L M N) ⇒ (fv_trm L) \u (fv_trm M) \u (fv_trm N)
  | (t_cast M A p B) ⇒ (fv_trm M)
  | (t_blame p) ⇒ {}
end.

Fixpoint fv_ictrm (iCL5:ictrm) : vars :=
  match iCL5 with
  | ictrm_hole{}
  | (ictrm_binop_left iCM iN) ⇒ (fv_ictrm iCM) \u (fv_itrm iN)
  | (ictrm_binop_right iM iCN) ⇒ (fv_itrm iM) \u (fv_ictrm iCN)
  | (ictrm_abs iA iCN) ⇒ (fv_ictrm iCN)
  | (ictrm_app_left iCL iM) ⇒ (fv_ictrm iCL) \u (fv_itrm iM)
  | (ictrm_app_right iL iCM) ⇒ (fv_itrm iL) \u (fv_ictrm iCM)
end.

Fixpoint fv_ctrm (CL5:ctrm) : vars :=
  match CL5 with
  | ctrm_hole{}
  | (ctrm_binop_left CM N) ⇒ (fv_ctrm CM) \u (fv_trm N)
  | (ctrm_binop_right M CN) ⇒ (fv_trm M) \u (fv_ctrm CN)
  | (ctrm_abs A CN) ⇒ (fv_ctrm CN)
  | (ctrm_app_left CL M) ⇒ (fv_ctrm CL) \u (fv_trm M)
  | (ctrm_app_right L CM) ⇒ (fv_trm L) \u (fv_ctrm CM)
  | (ctrm_lift CM) ⇒ (fv_ctrm CM)
  | (ctrm_case_scrutinee CL M N) ⇒ (fv_ctrm CL) \u (fv_trm M) \u (fv_trm N)
  | (ctrm_case_null L CM N) ⇒ (fv_trm L) \u (fv_ctrm CM) \u (fv_trm N)
  | (ctrm_case_nonnull L M CN) ⇒ (fv_trm L) \u (fv_trm M) \u (fv_ctrm CN)
  | (ctrm_cast CM A p B) ⇒ (fv_ctrm CM)
end.

substitutions
Fixpoint subst_itrm (iL5:itrm) (ix5:ivar) (iL_6:itrm) {struct iL_6} : itrm :=
  match iL_6 with
  | (itrm_var_b nat) ⇒ itrm_var_b nat
  | (itrm_var_f ix) ⇒ (if eq_var ix ix5 then iL5 else (itrm_var_f ix))
  | (itrm_const c) ⇒ itrm_const c
  | (itrm_binop iM iN) ⇒ itrm_binop (subst_itrm iL5 ix5 iM) (subst_itrm iL5 ix5 iN)
  | (itrm_abs iA iN) ⇒ itrm_abs iA (subst_itrm iL5 ix5 iN)
  | (itrm_app iL iM) ⇒ itrm_app (subst_itrm iL5 ix5 iL) (subst_itrm iL5 ix5 iM)
  | itrm_nullitrm_null
end.

Fixpoint subst_trm (L5:trm) (x5:var) (L_6:trm) {struct L_6} : trm :=
  match L_6 with
  | (t_var_b nat) ⇒ t_var_b nat
  | (t_var_f x) ⇒ (if eq_var x x5 then L5 else (t_var_f x))
  | (t_const c) ⇒ t_const c
  | (t_binop M N) ⇒ t_binop (subst_trm L5 x5 M) (subst_trm L5 x5 N)
  | (t_abs A N) ⇒ t_abs A (subst_trm L5 x5 N)
  | (t_app L M) ⇒ t_app (subst_trm L5 x5 L) (subst_trm L5 x5 M)
  | t_nullt_null
  | (t_lift M) ⇒ t_lift (subst_trm L5 x5 M)
  | (t_case L M N) ⇒ t_case (subst_trm L5 x5 L) (subst_trm L5 x5 M) (subst_trm L5 x5 N)
  | (t_cast M A p B) ⇒ t_cast (subst_trm L5 x5 M) A p B
  | (t_blame p) ⇒ t_blame p
end.

Fixpoint subst_ictrm (iL5:itrm) (ix5:ivar) (iCL5:ictrm) {struct iCL5} : ictrm :=
  match iCL5 with
  | ictrm_holeictrm_hole
  | (ictrm_binop_left iCM iN) ⇒ ictrm_binop_left (subst_ictrm iL5 ix5 iCM) (subst_itrm iL5 ix5 iN)
  | (ictrm_binop_right iM iCN) ⇒ ictrm_binop_right (subst_itrm iL5 ix5 iM) (subst_ictrm iL5 ix5 iCN)
  | (ictrm_abs iA iCN) ⇒ ictrm_abs iA (subst_ictrm iL5 ix5 iCN)
  | (ictrm_app_left iCL iM) ⇒ ictrm_app_left (subst_ictrm iL5 ix5 iCL) (subst_itrm iL5 ix5 iM)
  | (ictrm_app_right iL iCM) ⇒ ictrm_app_right (subst_itrm iL5 ix5 iL) (subst_ictrm iL5 ix5 iCM)
end.

Fixpoint subst_ctrm (L5:trm) (x5:var) (CL5:ctrm) {struct CL5} : ctrm :=
  match CL5 with
  | ctrm_holectrm_hole
  | (ctrm_binop_left CM N) ⇒ ctrm_binop_left (subst_ctrm L5 x5 CM) (subst_trm L5 x5 N)
  | (ctrm_binop_right M CN) ⇒ ctrm_binop_right (subst_trm L5 x5 M) (subst_ctrm L5 x5 CN)
  | (ctrm_abs A CN) ⇒ ctrm_abs A (subst_ctrm L5 x5 CN)
  | (ctrm_app_left CL M) ⇒ ctrm_app_left (subst_ctrm L5 x5 CL) (subst_trm L5 x5 M)
  | (ctrm_app_right L CM) ⇒ ctrm_app_right (subst_trm L5 x5 L) (subst_ctrm L5 x5 CM)
  | (ctrm_lift CM) ⇒ ctrm_lift (subst_ctrm L5 x5 CM)
  | (ctrm_case_scrutinee CL M N) ⇒ ctrm_case_scrutinee (subst_ctrm L5 x5 CL) (subst_trm L5 x5 M) (subst_trm L5 x5 N)
  | (ctrm_case_null L CM N) ⇒ ctrm_case_null (subst_trm L5 x5 L) (subst_ctrm L5 x5 CM) (subst_trm L5 x5 N)
  | (ctrm_case_nonnull L M CN) ⇒ ctrm_case_nonnull (subst_trm L5 x5 L) (subst_trm L5 x5 M) (subst_ctrm L5 x5 CN)
  | (ctrm_cast CM A p B) ⇒ ctrm_cast (subst_ctrm L5 x5 CM) A p B
end.

definitions

Inductive compat : typ typ Prop :=
 | compat_base :
     compat (typ_def dtyp_base) (typ_def dtyp_base)
 | compat_null_r : (A:typ) (D:dtyp),
     compat A (typ_def D)
     compat A (typ_null D)
 | compat_null_l : (D:dtyp) (A:typ),
     compat (typ_def D) A
     compat (typ_null D) A
 | compat_arrow : (A B A' B':typ),
     compat A A'
     compat B B'
     compat (typ_def (dtyp_arrow A B)) (typ_def (dtyp_arrow A' B')).

Inductive typing : ctx trm typ Prop :=
 | typing_var : (G:ctx) (x:var) (A:typ),
      uniq G
      binds x A G
     typing G (t_var_f x) A
 | typing_constant : (G:ctx) (c:constant),
      uniq G
     typing G (t_const c) (typ_def dtyp_base)
 | typing_binop : (G:ctx) (M N:trm),
     typing G M (typ_def dtyp_base)
     typing G N (typ_def dtyp_base)
     typing G (t_binop M N) (typ_def dtyp_base)
 | typing_abs : (L:vars) (G:ctx) (A:typ) (N:trm) (B:typ),
      ( x , x \notin L typing (( x ¬ A )++ G ) ( open_trm_wrt_trm N (t_var_f x) ) B )
     typing G (t_abs A N) (typ_def (dtyp_arrow A B))
 | typing_app : (G:ctx) (L M:trm) (B A:typ),
     typing G L (typ_def (dtyp_arrow A B))
     typing G M A
     typing G (t_app L M) B
 | typing_null : (G:ctx) (D:dtyp),
      uniq G
     typing G t_null (typ_null D)
 | typing_lift : (G:ctx) (M:trm) (D:dtyp),
     typing G M (typ_def D)
     typing G (t_lift M) (typ_null D)
 | typing_case : (L:vars) (G:ctx) (L' M N:trm) (A:typ) (D:dtyp),
     typing G L' (typ_null D)
     typing G M A
      ( x , x \notin L typing (( x ¬ (typ_def D) )++ G ) ( open_trm_wrt_trm N (t_var_f x) ) A )
     typing G (t_case L' M N) A
 | typing_cast : (G:ctx) (M:trm) (A:typ) (p:label) (B:typ),
     typing G M A
     compat A B
     typing G ( (t_cast M A p B) ) B
 | typing_blame : (G:ctx) (p:label) (A:typ),
      uniq G
     typing G (t_blame p) A.

Inductive neglabel : label label Prop :=
 | nl_pos_to_neg : (bl:blamelabel),
     neglabel (label_name bl) (label_not_label bl)
 | nl_neg_to_pos : (bl:blamelabel),
     neglabel (label_not_label bl) (label_name bl).

Inductive step : trm trm Prop :=
 | step_binop : (c:constant) (V W:trm),
     Is_true (is_val_of_trm V)
     Is_true (is_val_of_trm W)
     lc_trm V
     lc_trm W
     step (t_binop V W) (t_const c)
 | step_app : (A:typ) (N V:trm),
     Is_true (is_val_of_trm V)
     lc_trm (t_abs A N)
     lc_trm V
     step (t_app ( (t_abs A N) ) V) ( (open_trm_wrt_trm N V ) )
 | step_wrap : (A B:typ) (p:label) (A' B':typ) (p':label) (V W:trm),
     Is_true (is_val_of_trm V)
     Is_true (is_val_of_trm W)
     lc_trm V
     lc_trm W
     neglabel p p'
     step (t_app ( (t_cast V ( (typ_def (dtyp_arrow A B)) ) p ( (typ_def (dtyp_arrow A' B')) ) ) ) W) (t_cast ( (t_app V ( (t_cast W A' p' A) ) ) ) B p B')
 | step_cast_null : (D:dtyp) (p:label) (E:dtyp),
     step ( (t_cast t_null (typ_null D) p (typ_null E)) ) t_null
 | step_cast_lift : (D:dtyp) (p:label) (E:dtyp) (V:trm),
     Is_true (is_val_of_trm V)
     lc_trm V
     step ( (t_cast ( (t_lift V) ) (typ_null D) p (typ_null E)) ) (t_lift ( (t_cast V (typ_def D) p (typ_def E)) ) )
 | step_downcast_null : (D:dtyp) (p:label) (E:dtyp),
     step ( (t_cast t_null (typ_null D) p (typ_def E)) ) (t_blame p)
 | step_downcast_lift : (D:dtyp) (p:label) (E:dtyp) (V:trm),
     Is_true (is_val_of_trm V)
     lc_trm V
     step ( (t_cast ( (t_lift V) ) (typ_null D) p (typ_def E)) ) ( (t_cast V (typ_def D) p (typ_def E)) )
 | step_upcast : (D:dtyp) (p:label) (E:dtyp) (V:trm),
     Is_true (is_val_of_trm V)
     lc_trm V
     step ( (t_cast V (typ_def D) p (typ_null E)) ) (t_lift ( (t_cast V (typ_def D) p (typ_def E)) ) )
 | step_cast_base : (p:label) (V:trm),
     Is_true (is_val_of_trm V)
     lc_trm V
     step ( (t_cast V (typ_def dtyp_base) p (typ_def dtyp_base)) ) V
 | step_case_null : (M N:trm),
     lc_trm (t_case t_null M N)
     lc_trm M
     step (t_case t_null M N) M
 | step_case_lift : (M N V:trm),
     Is_true (is_val_of_trm V)
     lc_trm M
     lc_trm (t_case ( (t_lift V) ) M N)
     lc_trm V
     step (t_case ( (t_lift V) ) M N) ( (open_trm_wrt_trm N V ) )
 | step_appL_ctx : (M N M':trm),
     lc_trm N
     step M M'
     step (t_app M N) (t_app M' N)
 | step_appL_err : (p:label) (N:trm),
     lc_trm N
     step (t_app ( (t_blame p) ) N) (t_blame p)
 | step_appR_ctx : (N N' V:trm),
     Is_true (is_val_of_trm V)
     lc_trm V
     step N N'
     step (t_app V N) (t_app V N')
 | step_appR_err : (p:label) (V:trm),
     Is_true (is_val_of_trm V)
     lc_trm V
     step (t_app V ( (t_blame p) ) ) (t_blame p)
 | step_cast_ctx : (M:trm) (A:typ) (p:label) (B:typ) (M':trm),
     step M M'
     step ( (t_cast M A p B) ) ( (t_cast M' A p B) )
 | step_cast_err : (p:label) (A:typ) (q:label) (B:typ),
     step (t_cast ( (t_blame p) ) A q B) (t_blame p)
 | step_case_ctx : (L M N L':trm),
     lc_trm (t_case L M N)
     lc_trm M
     step L L'
     step (t_case L M N) (t_case L' M N)
 | step_case_err : (p:label) (M N:trm),
     lc_trm M
     lc_trm (t_case ( (t_blame p) ) M N)
     step (t_case ( (t_blame p) ) M N) (t_blame p)
 | step_lift_ctx : (M M':trm),
     step M M'
     step (t_lift M) (t_lift M')
 | step_lift_err : (p:label),
     step (t_lift ( (t_blame p) ) ) (t_blame p)
 | step_binopL_ctx : (M N M':trm),
     lc_trm N
     step M M'
     step (t_binop M N) (t_binop M' N)
 | step_binopL_err : (p:label) (N:trm),
     lc_trm N
     step (t_binop ( (t_blame p) ) N) (t_blame p)
 | step_binopR_ctx : (N N' V:trm),
     Is_true (is_val_of_trm V)
     lc_trm V
     step N N'
     step (t_binop V N) (t_binop V N')
 | step_binopR_err : (p:label) (V:trm),
     Is_true (is_val_of_trm V)
     lc_trm V
     step (t_binop V ( (t_blame p) ) ) (t_blame p).

Inductive subtyp : typ typ Prop :=
 | subtyp_base :
     subtyp (typ_def dtyp_base) (typ_def dtyp_base)
 | subtyp_null_sup : (D E:dtyp),
     subtyp (typ_def D) (typ_def E)
     subtyp (typ_def D) (typ_null E)
 | subtyp_null : (D E:dtyp),
     subtyp (typ_def D) (typ_def E)
     subtyp (typ_null D) (typ_null E)
 | subtyp_arrow : (A B A' B':typ),
     subtyp A' A
     subtyp B B'
     subtyp (typ_def (dtyp_arrow A B)) (typ_def (dtyp_arrow A' B')).

Inductive subtyp_n : typ typ Prop :=
 | subtyp_n_base :
     subtyp_n (typ_def dtyp_base) (typ_def dtyp_base)
 | subtyp_n_null_sup : (D E:dtyp),
     subtyp_n (typ_def D) (typ_def E)
     subtyp_n (typ_def D) (typ_null E)
 | subtyp_n_null : (D E:dtyp),
     subtyp_n (typ_def D) (typ_def E)
     subtyp_n (typ_null D) (typ_null E)
 | subtyp_n_arrow : (A B A' B':typ),
     subtyp_n A A'
     subtyp_n B B'
     subtyp_n (typ_def (dtyp_arrow A B)) (typ_def (dtyp_arrow A' B')).

Inductive subtyp_pos : typ typ Prop :=
 | subtyp_posbase :
     subtyp_pos (typ_def dtyp_base) (typ_def dtyp_base)
 | subtyp_posnull_sup : (D E:dtyp),
     subtyp_pos (typ_def D) (typ_def E)
     subtyp_pos (typ_def D) (typ_null E)
 | subtyp_posnull : (D E:dtyp),
     subtyp_pos (typ_def D) (typ_def E)
     subtyp_pos (typ_null D) (typ_null E)
 | subtyp_posarrow : (A B A' B':typ),
     subtyp_neg A' A
     subtyp_pos B B'
     subtyp_pos (typ_def (dtyp_arrow A B)) (typ_def (dtyp_arrow A' B'))
with subtyp_neg : typ typ Prop :=
 | subtyp_negbase :
     subtyp_neg (typ_def dtyp_base) (typ_def dtyp_base)
 | subtyp_negnull_sub : (D E:dtyp),
     subtyp_neg (typ_def D) (typ_def E)
     subtyp_neg (typ_null D) (typ_def E)
 | subtyp_negnull_sup : (D E:dtyp),
     subtyp_neg (typ_def D) (typ_def E)
     subtyp_neg (typ_def D) (typ_null E)
 | subtyp_negnull : (D E:dtyp),
     subtyp_neg (typ_def D) (typ_def E)
     subtyp_neg (typ_null D) (typ_null E)
 | subtyp_negarrow : (A B A' B':typ),
     subtyp_pos A' A
     subtyp_neg B B'
     subtyp_neg (typ_def (dtyp_arrow A B)) (typ_def (dtyp_arrow A' B')).

Inductive ityping : ictx itrm ityp Prop :=
 | ityping_var : (iG:ictx) (ix:ivar) (iA:ityp),
      uniq iG
      binds ix iA iG
     ityping iG (itrm_var_f ix) iA
 | ityping_base : (iG:ictx) (c:constant),
      uniq iG
     ityping iG (itrm_const c) ityp_base
 | ityping_binop : (iG:ictx) (iM iN:itrm),
     ityping iG iM ityp_base
     ityping iG iN ityp_base
     ityping iG (itrm_binop iM iN) ityp_base
 | ityping_abs : (L:vars) (iG:ictx) (iA:ityp) (iN:itrm) (iB:ityp),
      ( ix , ix \notin L ityping (( ix ¬ iA )++ iG ) ( open_itrm_wrt_itrm iN (itrm_var_f ix) ) iB )
     ityping iG (itrm_abs iA iN) (ityp_arrow iA iB)
 | ityping_app : (iG:ictx) (iL iM:itrm) (iB iA:ityp),
     ityping iG iL (ityp_arrow iA iB)
     ityping iG iM iA
     ityping iG (itrm_app iL iM) iB
 | ityping_null : (iG:ictx) (iA:ityp),
      uniq iG
     ityping iG itrm_null iA.

Inductive ctyping : ctx typ ctx ctrm typ Prop :=
 | ctyping_hole : (G:ctx) (A:typ),
      uniq G
     ctyping G A G ctrm_hole A
 | ctyping_binop_left : (G':ctx) (A':typ) (G:ctx) (CM:ctrm) (N:trm),
     ctyping G' A' G CM (typ_def dtyp_base)
     typing G N (typ_def dtyp_base)
     ctyping G' A' G (ctrm_binop_left CM N) (typ_def dtyp_base)
 | ctyping_binop_right : (G':ctx) (A':typ) (G:ctx) (M:trm) (CN:ctrm),
     typing G M (typ_def dtyp_base)
     ctyping G' A' G CN (typ_def dtyp_base)
     ctyping G' A' G (ctrm_binop_right M CN) (typ_def dtyp_base)
 | ctyping_abs : (L:vars) (G':ctx) (A':typ) (G:ctx) (A:typ) (CN:ctrm) (B:typ),
      ( x , x \notin L ctyping G' A' (( x ¬ A )++ G ) ( open_ctrm_wrt_trm CN (t_var_f x) ) B )
     ctyping G' A' G (ctrm_abs A CN) (typ_def (dtyp_arrow A B))
 | ctyping_app_left : (G':ctx) (A':typ) (G:ctx) (CL:ctrm) (M:trm) (B A:typ),
     ctyping G' A' G CL (typ_def (dtyp_arrow A B))
     typing G M A
     ctyping G' A' G (ctrm_app_left CL M) B
 | ctyping_app_right : (G':ctx) (A':typ) (G:ctx) (L:trm) (CM:ctrm) (B A:typ),
     typing G L (typ_def (dtyp_arrow A B))
     ctyping G' A' G CM A
     ctyping G' A' G (ctrm_app_right L CM) B
 | ctyping_lift : (G':ctx) (A':typ) (G:ctx) (CM:ctrm) (D:dtyp),
     ctyping G' A' G CM (typ_def D)
     ctyping G' A' G (ctrm_lift CM) (typ_null D)
 | ctyping_case_scrutinee : (L:vars) (G':ctx) (A':typ) (G:ctx) (CL':ctrm) (M N:trm) (A:typ) (D:dtyp),
     ctyping G' A' G CL' (typ_null D)
     typing G M A
      ( x , x \notin L typing (( x ¬ (typ_def D) )++ G ) ( open_trm_wrt_trm N (t_var_f x) ) A )
     ctyping G' A' G (ctrm_case_scrutinee CL' M N) A
 | ctyping_case_null : (L:vars) (G':ctx) (A':typ) (G:ctx) (L':trm) (CM:ctrm) (N:trm) (A:typ) (D:dtyp),
     typing G L' (typ_null D)
     ctyping G' A' G CM A
      ( x , x \notin L typing (( x ¬ (typ_def D) )++ G ) ( open_trm_wrt_trm N (t_var_f x) ) A )
     ctyping G' A' G (ctrm_case_null L' CM N) A
 | ctyping_case_nonnull : (L:vars) (G':ctx) (A':typ) (G:ctx) (L' M:trm) (CN:ctrm) (A:typ) (D:dtyp),
     typing G L' (typ_null D)
     typing G M A
      ( x , x \notin L ctyping G' A' (( x ¬ (typ_def D) )++ G ) ( open_ctrm_wrt_trm CN (t_var_f x) ) A )
     ctyping G' A' G (ctrm_case_nonnull L' M CN) A
 | ctyping_cast : (G':ctx) (A':typ) (G:ctx) (CM:ctrm) (A:typ) (p:label) (B:typ),
     ctyping G' A' G CM A
     compat A B
     ctyping G' A' G ( (ctrm_cast CM A p B) ) B.

Inductive ictyping : ictx ityp ictx ictrm ityp Prop :=
 | ictyping_hole : (iG:ictx) (iA:ityp),
      uniq iG
     ictyping iG iA iG ictrm_hole iA
 | ictyping_binop_left : (iG':ictx) (iA':ityp) (iG:ictx) (iCM:ictrm) (iN:itrm),
     ictyping iG' iA' iG iCM ityp_base
     ityping iG iN ityp_base
     ictyping iG' iA' iG (ictrm_binop_left iCM iN) ityp_base
 | ictyping_binop_right : (iG':ictx) (iA':ityp) (iG:ictx) (iM:itrm) (iCN:ictrm),
     ityping iG iM ityp_base
     ictyping iG' iA' iG iCN ityp_base
     ictyping iG' iA' iG (ictrm_binop_right iM iCN) ityp_base
 | ictyping_abs : (L:vars) (iG':ictx) (iA':ityp) (iG:ictx) (iA:ityp) (iCN:ictrm) (iB:ityp),
      ( ix , ix \notin L ictyping iG' iA' (( ix ¬ iA )++ iG ) ( open_ictrm_wrt_itrm iCN (itrm_var_f ix) ) iB )
     ictyping iG' iA' iG (ictrm_abs iA iCN) (ityp_arrow iA iB)
 | ictyping_app_left : (iG':ictx) (iA':ityp) (iG:ictx) (iCL:ictrm) (iM:itrm) (iB iA:ityp),
     ictyping iG' iA' iG iCL (ityp_arrow iA iB)
     ityping iG iM iA
     ictyping iG' iA' iG (ictrm_app_left iCL iM) iB
 | ictyping_app_right : (iG':ictx) (iA':ityp) (iG:ictx) (iL:itrm) (iCM:ictrm) (iB iA:ityp),
     ityping iG iL (ityp_arrow iA iB)
     ictyping iG' iA' iG iCM iA
     ictyping iG' iA' iG (ictrm_app_right iL iCM) iB.

infrastructure