LNgen.Fsub_ott

(* generated by Ott 0.30, locally-nameless lngen from: Fsub.ott *)
Require Import Metalib.Metatheory.

Definition typvar : Set := var.
Definition expvar : Set := var.

Inductive typ : Set :=
 | typ_top : typ
 | typ_var_b (_:nat)
 | typ_var_f (X:typvar)
 | typ_arrow (T1:typ) (T2:typ)
 | typ_all (T1:typ) (T2:typ)
 | typ_sum (T1:typ) (T2:typ).

Inductive binding : Set :=
 | bind_sub (T:typ)
 | bind_typ (T:typ).

Inductive exp : Set :=
 | exp_var_b (_:nat)
 | exp_var_f (x:expvar)
 | exp_abs (T:typ) (e:exp)
 | exp_app (e1:exp) (e2:exp)
 | exp_tabs (T:typ) (e:exp)
 | exp_tapp (e:exp) (T:typ)
 | exp_let (e1:exp) (e2:exp)
 | exp_inl (e:exp)
 | exp_inr (e:exp)
 | exp_case (e:exp) (e2:exp) (e3:exp).

Definition env : Set := list (atom*binding).

(* EXPERIMENTAL *)

Fixpoint is_value_of_exp (e_5:exp) : Prop :=
  match e_5 with
  | (exp_var_b nat) => False
  | (exp_var_f x) => False
  | (exp_abs T e) => (True)
  | (exp_app e1 e2) => False
  | (exp_tabs T e) => (True)
  | (exp_tapp e T) => False
  | (exp_let e1 e2) => False
  | (exp_inl e) => ((is_value_of_exp e))
  | (exp_inr e) => ((is_value_of_exp e))
  | (exp_case e e2 e3) => False
end.

Fixpoint open_typ_wrt_typ_rec (k:nat) (T_5:typ) (T__6:typ) {struct T__6}: typ :=
  match T__6 with
  | typ_top => typ_top
  | (typ_var_b nat) =>
      match lt_eq_lt_dec nat k with
        | inleft (left _) => typ_var_b nat
        | inleft (right _) => T_5
        | inright _ => typ_var_b (nat - 1)
      end
  | (typ_var_f X) => typ_var_f X
  | (typ_arrow T1 T2) => typ_arrow (open_typ_wrt_typ_rec k T_5 T1) (open_typ_wrt_typ_rec k T_5 T2)
  | (typ_all T1 T2) => typ_all (open_typ_wrt_typ_rec k T_5 T1) (open_typ_wrt_typ_rec (S k) T_5 T2)
  | (typ_sum T1 T2) => typ_sum (open_typ_wrt_typ_rec k T_5 T1) (open_typ_wrt_typ_rec k T_5 T2)
end.

Definition open_binding_wrt_typ_rec (k:nat) (T5:typ) (b5:binding) : binding :=
  match b5 with
  | (bind_sub T) => bind_sub (open_typ_wrt_typ_rec k T5 T)
  | (bind_typ T) => bind_typ (open_typ_wrt_typ_rec k T5 T)
end.

Fixpoint open_exp_wrt_exp_rec (k:nat) (e_5:exp) (e__6:exp) {struct e__6}: exp :=
  match e__6 with
  | (exp_var_b nat) =>
      match lt_eq_lt_dec nat k with
        | inleft (left _) => exp_var_b nat
        | inleft (right _) => e_5
        | inright _ => exp_var_b (nat - 1)
      end
  | (exp_var_f x) => exp_var_f x
  | (exp_abs T e) => exp_abs T (open_exp_wrt_exp_rec (S k) e_5 e)
  | (exp_app e1 e2) => exp_app (open_exp_wrt_exp_rec k e_5 e1) (open_exp_wrt_exp_rec k e_5 e2)
  | (exp_tabs T e) => exp_tabs T (open_exp_wrt_exp_rec k e_5 e)
  | (exp_tapp e T) => exp_tapp (open_exp_wrt_exp_rec k e_5 e) T
  | (exp_let e1 e2) => exp_let (open_exp_wrt_exp_rec k e_5 e1) (open_exp_wrt_exp_rec (S k) e_5 e2)
  | (exp_inl e) => exp_inl (open_exp_wrt_exp_rec k e_5 e)
  | (exp_inr e) => exp_inr (open_exp_wrt_exp_rec k e_5 e)
  | (exp_case e e2 e3) => exp_case (open_exp_wrt_exp_rec k e_5 e) (open_exp_wrt_exp_rec (S k) e_5 e2) (open_exp_wrt_exp_rec (S k) e_5 e3)
end.

Fixpoint open_exp_wrt_typ_rec (k:nat) (T_5:typ) (e_5:exp) {struct e_5}: exp :=
  match e_5 with
  | (exp_var_b nat) => exp_var_b nat
  | (exp_var_f x) => exp_var_f x
  | (exp_abs T e) => exp_abs (open_typ_wrt_typ_rec k T_5 T) (open_exp_wrt_typ_rec k T_5 e)
  | (exp_app e1 e2) => exp_app (open_exp_wrt_typ_rec k T_5 e1) (open_exp_wrt_typ_rec k T_5 e2)
  | (exp_tabs T e) => exp_tabs (open_typ_wrt_typ_rec k T_5 T) (open_exp_wrt_typ_rec (S k) T_5 e)
  | (exp_tapp e T) => exp_tapp (open_exp_wrt_typ_rec k T_5 e) (open_typ_wrt_typ_rec k T_5 T)
  | (exp_let e1 e2) => exp_let (open_exp_wrt_typ_rec k T_5 e1) (open_exp_wrt_typ_rec k T_5 e2)
  | (exp_inl e) => exp_inl (open_exp_wrt_typ_rec k T_5 e)
  | (exp_inr e) => exp_inr (open_exp_wrt_typ_rec k T_5 e)
  | (exp_case e e2 e3) => exp_case (open_exp_wrt_typ_rec k T_5 e) (open_exp_wrt_typ_rec k T_5 e2) (open_exp_wrt_typ_rec k T_5 e3)
end.

Definition open_binding_wrt_typ T5 b5 := open_binding_wrt_typ_rec 0 b5 T5.

Definition open_exp_wrt_exp e_5 e__6 := open_exp_wrt_exp_rec 0 e__6 e_5.

Definition open_exp_wrt_typ T_5 e_5 := open_exp_wrt_typ_rec 0 e_5 T_5.

Definition open_typ_wrt_typ T_5 T__6 := open_typ_wrt_typ_rec 0 T__6 T_5.

(* defns LC_typ *)
Inductive lc_typ : typ -> Prop := (* defn lc_typ *)
 | lc_typ_top :
     (lc_typ typ_top)
 | lc_typ_var_f : forall (X:typvar),
     (lc_typ (typ_var_f X))
 | lc_typ_arrow : forall (T1 T2:typ),
     (lc_typ T1) ->
     (lc_typ T2) ->
     (lc_typ (typ_arrow T1 T2))
 | lc_typ_all : forall (T1 T2:typ),
     (lc_typ T1) ->
      ( forall X , lc_typ ( open_typ_wrt_typ T2 (typ_var_f X) ) ) ->
     (lc_typ (typ_all T1 T2))
 | lc_typ_sum : forall (T1 T2:typ),
     (lc_typ T1) ->
     (lc_typ T2) ->
     (lc_typ (typ_sum T1 T2)).

(* defns LC_binding *)
Inductive lc_binding : binding -> Prop := (* defn lc_binding *)
 | lc_bind_sub : forall (T:typ),
     (lc_typ T) ->
     (lc_binding (bind_sub T))
 | lc_bind_typ : forall (T:typ),
     (lc_typ T) ->
     (lc_binding (bind_typ T)).

(* defns LC_exp *)
Inductive lc_exp : exp -> Prop := (* defn lc_exp *)
 | lc_exp_var_f : forall (x:expvar),
     (lc_exp (exp_var_f x))
 | lc_exp_abs : forall (T:typ) (e:exp),
     (lc_typ T) ->
      ( forall x , lc_exp ( open_exp_wrt_exp e (exp_var_f x) ) ) ->
     (lc_exp (exp_abs T e))
 | lc_exp_app : forall (e1 e2:exp),
     (lc_exp e1) ->
     (lc_exp e2) ->
     (lc_exp (exp_app e1 e2))
 | lc_exp_tabs : forall (T:typ) (e:exp),
     (lc_typ T) ->
      ( forall X , lc_exp ( open_exp_wrt_typ e (typ_var_f X) ) ) ->
     (lc_exp (exp_tabs T e))
 | lc_exp_tapp : forall (e:exp) (T:typ),
     (lc_exp e) ->
     (lc_typ T) ->
     (lc_exp (exp_tapp e T))
 | lc_exp_let : forall (e1 e2:exp),
     (lc_exp e1) ->
      ( forall x , lc_exp ( open_exp_wrt_exp e2 (exp_var_f x) ) ) ->
     (lc_exp (exp_let e1 e2))
 | lc_exp_inl : forall (e:exp),
     (lc_exp e) ->
     (lc_exp (exp_inl e))
 | lc_exp_inr : forall (e:exp),
     (lc_exp e) ->
     (lc_exp (exp_inr e))
 | lc_exp_case : forall (e e2 e3:exp),
     (lc_exp e) ->
      ( forall x , lc_exp ( open_exp_wrt_exp e2 (exp_var_f x) ) ) ->
      ( forall y , lc_exp ( open_exp_wrt_exp e3 (exp_var_f y) ) ) ->
     (lc_exp (exp_case e e2 e3)).

Fixpoint fv_typ_in_typ (T_5:typ) : vars :=
  match T_5 with
  | typ_top => {}
  | (typ_var_b nat) => {}
  | (typ_var_f X) => {{X}}
  | (typ_arrow T1 T2) => (fv_typ_in_typ T1) \u (fv_typ_in_typ T2)
  | (typ_all T1 T2) => (fv_typ_in_typ T1) \u (fv_typ_in_typ T2)
  | (typ_sum T1 T2) => (fv_typ_in_typ T1) \u (fv_typ_in_typ T2)
end.

Definition fv_typ_in_binding (b5:binding) : vars :=
  match b5 with
  | (bind_sub T) => (fv_typ_in_typ T)
  | (bind_typ T) => (fv_typ_in_typ T)
end.

Fixpoint fv_exp_in_exp (e_5:exp) : vars :=
  match e_5 with
  | (exp_var_b nat) => {}
  | (exp_var_f x) => {{x}}
  | (exp_abs T e) => (fv_exp_in_exp e)
  | (exp_app e1 e2) => (fv_exp_in_exp e1) \u (fv_exp_in_exp e2)
  | (exp_tabs T e) => (fv_exp_in_exp e)
  | (exp_tapp e T) => (fv_exp_in_exp e)
  | (exp_let e1 e2) => (fv_exp_in_exp e1) \u (fv_exp_in_exp e2)
  | (exp_inl e) => (fv_exp_in_exp e)
  | (exp_inr e) => (fv_exp_in_exp e)
  | (exp_case e e2 e3) => (fv_exp_in_exp e) \u (fv_exp_in_exp e2) \u (fv_exp_in_exp e3)
end.

Fixpoint fv_typ_in_exp (e_5:exp) : vars :=
  match e_5 with
  | (exp_var_b nat) => {}
  | (exp_var_f x) => {}
  | (exp_abs T e) => (fv_typ_in_typ T) \u (fv_typ_in_exp e)
  | (exp_app e1 e2) => (fv_typ_in_exp e1) \u (fv_typ_in_exp e2)
  | (exp_tabs T e) => (fv_typ_in_typ T) \u (fv_typ_in_exp e)
  | (exp_tapp e T) => (fv_typ_in_exp e) \u (fv_typ_in_typ T)
  | (exp_let e1 e2) => (fv_typ_in_exp e1) \u (fv_typ_in_exp e2)
  | (exp_inl e) => (fv_typ_in_exp e)
  | (exp_inr e) => (fv_typ_in_exp e)
  | (exp_case e e2 e3) => (fv_typ_in_exp e) \u (fv_typ_in_exp e2) \u (fv_typ_in_exp e3)
end.

Fixpoint subst_typ_in_typ (T_5:typ) (X5:typvar) (T__6:typ) {struct T__6} : typ :=
  match T__6 with
  | typ_top => typ_top
  | (typ_var_b nat) => typ_var_b nat
  | (typ_var_f X) => (if eq_var X X5 then T_5 else (typ_var_f X))
  | (typ_arrow T1 T2) => typ_arrow (subst_typ_in_typ T_5 X5 T1) (subst_typ_in_typ T_5 X5 T2)
  | (typ_all T1 T2) => typ_all (subst_typ_in_typ T_5 X5 T1) (subst_typ_in_typ T_5 X5 T2)
  | (typ_sum T1 T2) => typ_sum (subst_typ_in_typ T_5 X5 T1) (subst_typ_in_typ T_5 X5 T2)
end.

Definition subst_typ_in_binding (T5:typ) (X5:typvar) (b5:binding) : binding :=
  match b5 with
  | (bind_sub T) => bind_sub (subst_typ_in_typ T5 X5 T)
  | (bind_typ T) => bind_typ (subst_typ_in_typ T5 X5 T)
end.

Fixpoint subst_exp_in_exp (e_5:exp) (x5:expvar) (e__6:exp) {struct e__6} : exp :=
  match e__6 with
  | (exp_var_b nat) => exp_var_b nat
  | (exp_var_f x) => (if eq_var x x5 then e_5 else (exp_var_f x))
  | (exp_abs T e) => exp_abs T (subst_exp_in_exp e_5 x5 e)
  | (exp_app e1 e2) => exp_app (subst_exp_in_exp e_5 x5 e1) (subst_exp_in_exp e_5 x5 e2)
  | (exp_tabs T e) => exp_tabs T (subst_exp_in_exp e_5 x5 e)
  | (exp_tapp e T) => exp_tapp (subst_exp_in_exp e_5 x5 e) T
  | (exp_let e1 e2) => exp_let (subst_exp_in_exp e_5 x5 e1) (subst_exp_in_exp e_5 x5 e2)
  | (exp_inl e) => exp_inl (subst_exp_in_exp e_5 x5 e)
  | (exp_inr e) => exp_inr (subst_exp_in_exp e_5 x5 e)
  | (exp_case e e2 e3) => exp_case (subst_exp_in_exp e_5 x5 e) (subst_exp_in_exp e_5 x5 e2) (subst_exp_in_exp e_5 x5 e3)
end.

Fixpoint subst_typ_in_exp (T_5:typ) (X5:typvar) (e_5:exp) {struct e_5} : exp :=
  match e_5 with
  | (exp_var_b nat) => exp_var_b nat
  | (exp_var_f x) => exp_var_f x
  | (exp_abs T e) => exp_abs (subst_typ_in_typ T_5 X5 T) (subst_typ_in_exp T_5 X5 e)
  | (exp_app e1 e2) => exp_app (subst_typ_in_exp T_5 X5 e1) (subst_typ_in_exp T_5 X5 e2)
  | (exp_tabs T e) => exp_tabs (subst_typ_in_typ T_5 X5 T) (subst_typ_in_exp T_5 X5 e)
  | (exp_tapp e T) => exp_tapp (subst_typ_in_exp T_5 X5 e) (subst_typ_in_typ T_5 X5 T)
  | (exp_let e1 e2) => exp_let (subst_typ_in_exp T_5 X5 e1) (subst_typ_in_exp T_5 X5 e2)
  | (exp_inl e) => exp_inl (subst_typ_in_exp T_5 X5 e)
  | (exp_inr e) => exp_inr (subst_typ_in_exp T_5 X5 e)
  | (exp_case e e2 e3) => exp_case (subst_typ_in_exp T_5 X5 e) (subst_typ_in_exp T_5 X5 e2) (subst_typ_in_exp T_5 X5 e3)
end.

(* defns Jwf_typ *)
Inductive wf_typ : env -> typ -> Prop := (* defn wf_typ *)
 | wf_typ_top : forall (E:env),
     wf_typ E typ_top
 | wf_typ_var : forall (E:env) (X:typvar) (U:typ),
      binds ( X ) ( (bind_sub U) ) ( E ) ->
     wf_typ E (typ_var_f X)
 | wf_typ_arrow : forall (E:env) (T1 T2:typ),
     wf_typ E T1 ->
     wf_typ E T2 ->
     wf_typ E (typ_arrow T1 T2)
 | wf_typ_all : forall (L:vars) (E:env) (T1 T2:typ),
     wf_typ E T1 ->
      ( forall X , X \notin L -> wf_typ ( X ~ (bind_sub T1) ++ E ) ( open_typ_wrt_typ T2 (typ_var_f X) ) ) ->
     wf_typ E (typ_all T1 T2)
 | wf_typ_sum : forall (E:env) (T1 T2:typ),
     wf_typ E T1 ->
     wf_typ E T2 ->
     wf_typ E (typ_sum T1 T2).

(* defns Jwf_env *)
Inductive wf_env : env -> Prop := (* defn wf_env *)
 | wf_env_empty :
     wf_env nil
 | wf_env_sub : forall (E:env) (X:typvar) (T:typ),
     wf_env E ->
     wf_typ E T ->
      ( X `notin` dom ( E )) ->
     wf_env ( X ~ (bind_sub T) ++ E )
 | wf_env_typ : forall (E:env) (x:expvar) (T:typ),
     wf_env E ->
     wf_typ E T ->
      ( x `notin` dom ( E )) ->
     wf_env ( x ~ (bind_typ T) ++ E ) .

(* defns Jsub *)
Inductive sub : env -> typ -> typ -> Prop := (* defn sub *)
 | sub_top : forall (E:env) (S:typ),
     wf_env E ->
     wf_typ E S ->
     sub E S typ_top
 | sub_refl_tvar : forall (E:env) (X:typvar),
     wf_env E ->
     wf_typ E (typ_var_f X) ->
     sub E (typ_var_f X) (typ_var_f X)
 | sub_trans_tvar : forall (E:env) (X:typvar) (T U:typ),
      binds ( X ) ( (bind_sub U) ) ( E ) ->
     sub E U T ->
     sub E (typ_var_f X) T
 | sub_arrow : forall (E:env) (S1 S2 T1 T2:typ),
     sub E T1 S1 ->
     sub E S2 T2 ->
     sub E (typ_arrow S1 S2) (typ_arrow T1 T2)
 | sub_all : forall (L:vars) (E:env) (S1 S2 T1 T2:typ),
     sub E T1 S1 ->
      ( forall X , X \notin L -> sub ( X ~ (bind_sub T1) ++ E ) ( open_typ_wrt_typ S2 (typ_var_f X) ) ( open_typ_wrt_typ T2 (typ_var_f X) ) ) ->
     sub E (typ_all S1 S2) (typ_all T1 T2)
 | sub_sum : forall (E:env) (S1 S2 T1 T2:typ),
     sub E S1 T1 ->
     sub E S2 T2 ->
     sub E (typ_sum S1 S2) (typ_sum T1 T2).

(* defns Jtyping *)
Inductive typing : env -> exp -> typ -> Prop := (* defn typing *)
 | typing_var : forall (E:env) (x:expvar) (T:typ),
     wf_env E ->
      binds ( x ) ( (bind_typ T) ) ( E ) ->
     typing E (exp_var_f x) T
 | typing_abs : forall (L:vars) (E:env) (T1:typ) (e:exp) (T2:typ),
      ( forall x , x \notin L -> typing ( x ~ (bind_typ T1) ++ E ) ( open_exp_wrt_exp e (exp_var_f x) ) T2 ) ->
     typing E (exp_abs T1 e) (typ_arrow T1 T2)
 | typing_app : forall (E:env) (e1 e2:exp) (T2 T1:typ),
     typing E e1 (typ_arrow T1 T2) ->
     typing E e2 T1 ->
     typing E (exp_app e1 e2) T2
 | typing_tabs : forall (L:vars) (E:env) (T1:typ) (e:exp) (T2:typ),
      ( forall X , X \notin L -> typing ( X ~ (bind_sub T1) ++ E ) ( open_exp_wrt_typ e (typ_var_f X) ) ( open_typ_wrt_typ T2 (typ_var_f X) ) ) ->
     typing E (exp_tabs T1 e) (typ_all T1 T2)
 | typing_tapp : forall (E:env) (e1:exp) (T T2 T1:typ),
     typing E e1 (typ_all T1 T2) ->
     sub E T T1 ->
     typing E (exp_tapp e1 T) (open_typ_wrt_typ T2 T )
 | typing_sub : forall (E:env) (e:exp) (T S:typ),
     typing E e S ->
     sub E S T ->
     typing E e T
 | typing_let : forall (L:vars) (E:env) (e1 e2:exp) (T2 T1:typ),
     typing E e1 T1 ->
      ( forall x , x \notin L -> typing ( x ~ (bind_typ T1) ++ E ) ( open_exp_wrt_exp e2 (exp_var_f x) ) T2 ) ->
     typing E (exp_let e1 e2) T2
 | typing_inl : forall (E:env) (e1:exp) (T1 T2:typ),
     typing E e1 T1 ->
     wf_typ E T2 ->
     typing E (exp_inl e1) (typ_sum T1 T2)
 | typing_inr : forall (E:env) (e1:exp) (T1 T2:typ),
     typing E e1 T2 ->
     wf_typ E T1 ->
     typing E (exp_inr e1) (typ_sum T1 T2)
 | typing_case : forall (L:vars) (E:env) (e1 e2 e3:exp) (T T1 T2:typ),
     typing E e1 (typ_sum T1 T2) ->
      ( forall x , x \notin L -> typing ( x ~ (bind_typ T1) ++ E ) ( open_exp_wrt_exp e2 (exp_var_f x) ) T ) ->
      ( forall y , y \notin L -> typing ( y ~ (bind_typ T2) ++ E ) ( open_exp_wrt_exp e3 (exp_var_f y) ) T ) ->
     typing E (exp_case e1 e2 e3) T.

(* defns Jop *)
Inductive red : exp -> exp -> Prop := (* defn red *)
 | red_app_1 : forall (e1 e2 e1':exp),
     lc_exp e2 ->
     red e1 e1' ->
     red (exp_app e1 e2) (exp_app e1' e2)
 | red_app_2 : forall (e2 e2' v1:exp),
     is_value_of_exp v1 ->
     lc_exp v1 ->
     red e2 e2' ->
     red (exp_app v1 e2) (exp_app v1 e2')
 | red_tapp_1 : forall (e1:exp) (T:typ) (e1':exp),
     lc_typ T ->
     red e1 e1' ->
     red (exp_tapp e1 T) (exp_tapp e1' T)
 | red_abs : forall (T:typ) (e1 v2:exp),
     is_value_of_exp v2 ->
     lc_typ T ->
     lc_exp (exp_abs T e1) ->
     lc_exp v2 ->
     red (exp_app ( (exp_abs T e1) ) v2) (open_exp_wrt_exp e1 v2 )
 | red_tabs : forall (T1:typ) (e1:exp) (T2:typ),
     lc_typ T1 ->
     lc_exp (exp_tabs T1 e1) ->
     lc_typ T2 ->
     red (exp_tapp ( (exp_tabs T1 e1) ) T2) (open_exp_wrt_typ e1 T2 )
 | red_let_1 : forall (e1 e2 e1':exp),
     lc_exp (exp_let e1 e2) ->
     red e1 e1' ->
     red (exp_let e1 e2) (exp_let e1' e2)
 | red_let : forall (e2 v1:exp),
     is_value_of_exp v1 ->
     lc_exp (exp_let v1 e2) ->
     lc_exp v1 ->
     red (exp_let v1 e2) (open_exp_wrt_exp e2 v1 )
 | red_inl_1 : forall (e1 e1':exp),
     red e1 e1' ->
     red (exp_inl e1) (exp_inl e1')
 | red_inr_1 : forall (e1 e1':exp),
     red e1 e1' ->
     red (exp_inr e1) (exp_inr e1')
 | red_case_1 : forall (e1 e2 e3 e1':exp),
     lc_exp (exp_case e1 e2 e3) ->
     lc_exp (exp_case e1 e2 e3) ->
     red e1 e1' ->
     red (exp_case e1 e2 e3) (exp_case e1' e2 e3)
 | red_case_inl : forall (e2 e3 v1:exp),
     is_value_of_exp v1 ->
     lc_exp (exp_case (exp_inl v1) e2 e3) ->
     lc_exp (exp_case (exp_inl v1) e2 e3) ->
     lc_exp v1 ->
     red (exp_case (exp_inl v1) e2 e3) (open_exp_wrt_exp e2 v1 )
 | red_case_inr : forall (e2 e3 v1:exp),
     is_value_of_exp v1 ->
     lc_exp (exp_case (exp_inr v1) e2 e3) ->
     lc_exp (exp_case (exp_inr v1) e2 e3) ->
     lc_exp v1 ->
     red (exp_case (exp_inr v1) e2 e3) (open_exp_wrt_exp e3 v1 ) .

Hint Constructors wf_typ wf_env sub typing red lc_typ lc_binding lc_exp : core.