(* binders/ must be a subdirectory in the current working directory. *)  
Add LoadPath "binders".


Require Import Specif.
Require Import Metatheory.
Require Import Metatheory_Var.
Require Import OrderedType OrderedTypeEx.
Require Import Peano_dec.
Require Import cps_definitions_full.


(** Tactics for generating fresh variables *)

Ltac gather_vars :=
  let A := gather_vars_with (fun x : vars => x) in
  let B := gather_vars_with (fun x : var => {{ x }}) in
  let C := gather_vars_with (fun x : trm => fv x) in
  let D := gather_vars_with (fun x : val => fv_val x) in
  let E := gather_vars_with (fun x : cont => fv_cont x) in 
  let F := gather_vars_with (fun x : exp => fv_exp x) in
  let G := gather_vars_with (fun x : trm => fvc x) in
  let H := gather_vars_with (fun x : val => fvc_val x) in
  let I := gather_vars_with (fun x : cont => fvc_cont x) in 
  let J := gather_vars_with (fun x : exp => fvc_exp x) in
  constr:(A \u B \u C \u D \u E \u F \u G \u H \u I \u J).

Ltac pick_fresh X :=
  let L := gather_vars in (pick_fresh_gen L X).

Ltac pick_fresh_for L X :=
  let L := constr:L in (pick_fresh_gen L X).

Tactic Notation "apply_fresh" constr(T) "as" ident(x) :=
  apply_fresh_base T gather_vars x.

Tactic Notation "apply_fresh" "*" constr(T) "as" ident(x) :=
  apply_fresh T as x; auto*.


(** Substitution (of values!) for names *)

Fixpoint subst (r:trm) (x:var) (v:val) {struct r} : trm :=
match r with
| trm_term e => trm_term (subst_exp e x v)
end
with
subst_exp e x v {struct e} : exp :=
match e with
| cont_app c v' => cont_app (subst_cont c x v) (subst_val v' x v)
| trm_app r c => trm_app (subst r x v) (subst_cont c x v)
| val_app v0 v1 c => val_app (subst_val v0 x v) (subst_val v1 x v) (subst_cont c x v)
| elet z v0 e => elet z (subst_val v0 x v) (subst_exp e x v)
end
with
subst_val u x v {struct u} : val :=
match u with
| bvar w => bvar w
| fvar y => if x == y then v else fvar y 
| lam z r => lam z (subst r x v)
end
with
subst_cont c x v {struct c} : cont :=
match c with
| c_bid n => c_bid n
| c_fid n => c_fid n
| c_lam e => c_lam (subst_exp e x v)
end.

Notation "[ z ~> u ] t" := (subst t z u) (at level 68).

(** Substitution (of continuations!) for continuation names *)

Fixpoint substc (r:trm) (x:var) (c:cont) {struct r} : trm :=
match r with
| trm_term e => trm_term (substc_exp e x c)
end
with
substc_exp e x c {struct e} : exp :=
match e with
| cont_app c' v' => cont_app (substc_cont c' x c) (substc_val v' x c)
| trm_app r c' => trm_app (substc r x c) (substc_cont c' x c)
| val_app v0 v1 c' => val_app (substc_val v0 x c) (substc_val v1 x c) (substc_cont c' x c)
| elet z v e => elet z (substc_val v x c) (substc_exp e x c)
end
with
substc_val u x c {struct u} : val :=
match u with
| bvar w => bvar w
| fvar y => fvar y 
| lam z r => lam z (substc r x c)
end
with
substc_cont c' x c {struct c'} : cont :=
match c' with
| c_bid n => c_bid n
| c_fid y => if y == x then c else c_fid y
| c_lam e => c_lam (substc_exp e x c)
end.

(** Various auxiliary properties of substitutions *)

Ltac equ_inversion :=
match goal with
| [ H1 : ?x1 = ?y1 , H2 : ?x2 = ?y2 |- _ ] => inversion* H1; inversion* H2
| [ H : ?x = ?y |- _ ] => inversion* H
end.


Lemma open_exp_core :
forall e j v i u, i <> j ->
  open_exp j v e = open_exp i u (open_exp j v e) -> e = open_exp i u e.
Proof.
intro e.
apply trmexpind with
(P:= fun r => forall j v i u, i <> j ->
open_rec j v r = open_rec i u (open_rec j v r) -> r = open_rec i u r)
(P0:= fun e => forall j v i u, i <> j ->
open_exp j v e = open_exp i u (open_exp j v e) -> e = open_exp i u e)
(P1:= fun v0 => forall j v i u, i <> j ->
open_val j v v0 = open_val i u (open_val j v v0) -> v0 = open_val i u v0)
(P2:= fun c => forall j v i u, i <> j ->
open_cont j v c = open_cont i u (open_cont j v c) -> c = open_cont i u c)
; intros; simpl; equ_inversion; f_equal*.
case_nat*.
case_nat*.
Qed.

Lemma openc_exp_core :
forall e j v i u, i <> j ->
  openc_exp j v e = openc_exp i u (openc_exp j v e) -> e = openc_exp i u e.
Proof.
intro e.
apply trmexpind with
(P:= fun r => forall j v i u, i <> j ->
openc_rec j v r = openc_rec i u (openc_rec j v r) -> r = openc_rec i u r)
(P0:= fun e => forall j v i u, i <> j ->
openc_exp j v e = openc_exp i u (openc_exp j v e) -> e = openc_exp i u e)
(P1:= fun v0 => forall j v i u, i <> j ->
openc_val j v v0 = openc_val i u (openc_val j v v0) -> v0 = openc_val i u v0)
(P2:= fun c => forall j v i u, i <> j ->
openc_cont j v c = openc_cont i u (openc_cont j v c) -> c = openc_cont i u c)
; intros; simpl; equ_inversion; f_equal*.
case_nat*.
case_nat*.
Qed.

Lemma open_openc_exp_core :
forall e j c i u, i <> j ->
  openc_exp j c e = open_exp i u (openc_exp j c e) -> e = open_exp i u e.
Proof.
intro e.
apply trmexpind with
(P:= fun r => forall j c i u, i <> j ->
openc_rec j c r = open_rec i u (openc_rec j c r) -> r = open_rec i u r)
(P0:= fun e => forall j c i u, i <> j ->
openc_exp j c e = open_exp i u (openc_exp j c e) -> e = open_exp i u e)
(P1:= fun v0 => forall j c i u, i <> j ->
openc_val j c v0 = open_val i u (openc_val j c v0) -> v0 = open_val i u v0)
(P2:= fun c => forall j c' i u, i <> j ->
openc_cont j c' c = open_cont i u (openc_cont j c' c) -> c = open_cont i u c)
; intros; simpl; equ_inversion; f_equal*.
Qed.

Lemma openc_open_exp_core :
forall e j c i u, i <> j ->
  open_exp j c e = openc_exp i u (open_exp j c e) -> e = openc_exp i u e.
Proof.
intro e.
apply trmexpind with
(P:= fun r => forall j v i u, i <> j ->
open_rec j v r = openc_rec i u (open_rec j v r) -> r = openc_rec i u r)
(P0:= fun e => forall j v i u, i <> j ->
open_exp j v e = openc_exp i u (open_exp j v e) -> e = openc_exp i u e)
(P1:= fun v0 => forall j v i u, i <> j ->
open_val j v v0 = openc_val i u (open_val j v v0) -> v0 = openc_val i u v0)
(P2:= fun c => forall j v i u, i <> j ->
open_cont j v c = openc_cont i u (open_cont j v c) -> c = openc_cont i u c)
; intros; simpl; equ_inversion; f_equal*.
Qed.

Lemma open_rec_term_core :
forall e j v i u, i <> j ->
  open_rec j v e = open_rec i u (open_rec j v e) -> e = open_rec i u e.
Proof.
intro e.
apply trmind with
(P:= fun r => forall j v i u, i <> j ->
open_rec j v r = open_rec i u (open_rec j v r) -> r = open_rec i u r)
(P0:= fun e => forall j v i u, i <> j ->
open_exp j v e = open_exp i u (open_exp j v e) -> e = open_exp i u e)
(P1:= fun v0 => forall j v i u, i <> j ->
open_val j v v0 = open_val i u (open_val j v v0) -> v0 = open_val i u v0)
(P2:= fun c => forall j v i u, i <> j ->
open_cont j v c = open_cont i u (open_cont j v c) -> c = open_cont i u c)
; intros; simpl; equ_inversion; f_equal*.
case_nat*.
case_nat*.
Qed.

(** Substitution for a fresh name is identity. *)

Lemma subst_fresh : forall x t u, 
  x \notin fv t ->  subst t x u = t.
Proof.
intros x t u.
generalize x u; clear x u.
apply trmind with (P:= fun e => forall x u, x \notin fv e -> subst e x u = e)
(P0:= fun e => forall w v, w \notin fv_exp e -> subst_exp e w v = e)
(P1:= fun v => forall w v0, w \notin fv_val v -> subst_val v w v0 = v)
(P2:= fun c => forall w v, w \notin fv_cont c -> subst_cont c w v = c);
intros; simpls; f_equal*.
case_var*. 
(*notin_contradiction.*)
Qed.

Lemma subst_val_fresh : forall x e u, 
  x \notin fv_val e ->  subst_val e x u = e.
Proof.
intros x t u.
generalize x u; clear x u.
apply trmvalind with (P:= fun e => forall x u, x \notin fv e -> subst e x u = e)
(P0:= fun e => forall w v, w \notin fv_exp e -> subst_exp e w v = e)
(P1:= fun v => forall w v0, w \notin fv_val v -> subst_val v w v0 = v)
(P2:= fun c => forall w v, w \notin fv_cont c -> subst_cont c w v = c);
intros; simpls; f_equal*.
case_var*. 
(*notin_contradiction.*)
Qed.


Lemma subst_exp_fresh : forall x e u, 
  x \notin fv_exp e ->  subst_exp e x u = e.
Proof.
intros x e u.
generalize x u; clear x u.
apply trmexpind with (P:= fun e => forall x u, x \notin fv e -> subst e x u = e)
(P0:= fun e => forall w v, w \notin fv_exp e -> subst_exp e w v = e)
(P1:= fun v => forall w v0, w \notin fv_val v -> subst_val v w v0 = v)
(P2:= fun c => forall w v, w \notin fv_cont c -> subst_cont c w v = c);
intros; simpls; f_equal*.
case_var*.
(* notin_contradiction.*)
Qed.

Lemma subst_cont_fresh : forall x e u, 
  x \notin fv_cont e ->  subst_cont e x u = e.
Proof.
intros x e u.
generalize x u; clear x u.
apply trmcontind with (P:= fun e => forall x u, x \notin fv e -> subst e x u = e)
(P0:= fun e => forall w v, w \notin fv_exp e -> subst_exp e w v = e)
(P1:= fun v => forall w v0, w \notin fv_val v -> subst_val v w v0 = v)
(P2:= fun c => forall w v, w \notin fv_cont c -> subst_cont c w v = c);
intros; simpls; f_equal*.
case_var*. 
(*notin_contradiction.*)
Qed.

Lemma substc_cont_fresh : forall x e u, 
  x \notin fvc_cont e ->  substc_cont e x u = e.
Proof.
intros x e u.
generalize x u; clear x u.
apply trmcontind with (P:= fun e => forall x u, x \notin fvc e -> substc e x u = e)
(P0:= fun e => forall w v, w \notin fvc_exp e -> substc_exp e w v = e)
(P1:= fun v => forall w v0, w \notin fvc_val v -> substc_val v w v0 = v)
(P2:= fun c => forall w v, w \notin fvc_cont c -> substc_cont c w v = c);
intros; simpls; f_equal*.
case_var*. 
(*notin_contradiction.*)
Qed.

Lemma substc_exp_fresh : forall x e u, 
  x \notin fvc_exp e ->  substc_exp e x u = e.
Proof.
intros x e u.
generalize x u; clear x u.
apply trmexpind with (P:= fun e => forall x u, x \notin fvc e -> substc e x u = e)
(P0:= fun e => forall w v, w \notin fvc_exp e -> substc_exp e w v = e)
(P1:= fun v => forall w v0, w \notin fvc_val v -> substc_val v w v0 = v)
(P2:= fun c => forall w v, w \notin fvc_cont c -> substc_cont c w v = c);
intros; simpls; f_equal*.
case_var*.
(* notin_contradiction.*)
Qed.

Lemma open_rec_term : forall e,
  term_exp e -> (forall k u, open_exp k u e = e) /\ (forall k c, openc_exp k c e = e).
Proof.
intros e H.
apply termexpind with
(P:= fun e (H: term e) =>
(forall k v, open_rec k v e = e) /\ forall k c, openc_rec k c e = e)
(P0:= fun e (H:term_exp e) =>
(forall k v, open_exp k v e = e) /\ forall k c, openc_exp k c e = e)
(P1:= fun v (H: term_val v) =>
(forall k v0, open_val k v0 v = v) /\ forall k c, openc_val k c v = v)
(P2:= fun c (H: term_cont c) =>
((forall k v, open_cont k v c = c) /\ forall k c', openc_cont k c' c = c)); intros; simpl; f_equal*.
pick_fresh n.
notin_simpls.
split; intros.
assert (hh:=H0 n Fr).
destruct hh.
rewrite <- (@open_openc_exp_core e0 0 (c_fid n)); auto.
assert (hh:=H0 n Fr).
destruct hh.
rewrite <- (@openc_exp_core e0 0 (c_fid n)); auto.
(**)
destruct H0; destruct H1.
split; intros; f_equal*.
(**)
destruct H0; destruct H1.
split; intros; f_equal*.
(**)
destruct H0; destruct H1.
split; intros; f_equal*.
(**)
destruct H0.
split; intros; f_equal*.
(**)
destruct H0.
split; intros; f_equal*.
(**)
pick_fresh n.
notin_simpls.
split; intros.
assert (hh:=H0 n Fr).
destruct hh.
rewrite <- (@open_exp_core e0 0 (fvar n)); auto.
assert (hh:=H0 n Fr).
destruct hh.
rewrite <- (@openc_open_exp_core e0 0 (fvar n)); auto.
Qed.


Lemma term_openc :
forall e,  term e -> forall k v, openc_rec k v e = e.
Proof.
intros e H.
apply termind with
(P:= fun e (H: term e) =>
forall k v, openc_rec k v e = e)
(P0:= fun e (H: term_exp e) =>
forall k v, openc_exp k v e = e)
(P1:= fun v (H: term_val v) =>
forall k v0, openc_val k v0 v = v)
(P2:= fun c (H: term_cont c) =>
forall k v, openc_cont k v c = c)
(*(forall e L, c = c_lam e -> 
(forall x, x \notin L -> term_exp (open_exp 0 (fvar x) e)) -> 
forall k v, open_cont k v c = c))*)
; intros; subst; simpl; 
try rewrite H0; try rewrite H1; auto.
pick_fresh n.
notin_simpls.
assert (hh:=H0 n Fr).
rewrite <- (@openc_exp_core e0 0 (c_fid n)); auto.
(**)
rewrite H2; auto.
(**)
pick_fresh n.
notin_simpls.
assert (hh:=H0 n Fr).
rewrite <- (@openc_open_exp_core e0 0 (fvar n)); auto.
Qed.

Lemma term_openc_exp :
forall e,  term_exp e -> forall k v, openc_exp k v e = e.
Proof.
intros e H.
apply termexpind with
(P:= fun e (H: term e) =>
forall k v, openc_rec k v e = e)
(P0:= fun e (H: term_exp e) =>
forall k v, openc_exp k v e = e)
(P1:= fun v (H: term_val v) =>
forall k v0, openc_val k v0 v = v)
(P2:= fun c (H: term_cont c) =>
forall k v, openc_cont k v c = c)
(*(forall e L, c = c_lam e -> 
(forall x, x \notin L -> term_exp (open_exp 0 (fvar x) e)) -> 
forall k v, open_cont k v c = c))*)
; intros; subst; simpl; 
try rewrite H0; try rewrite H1; auto.
pick_fresh n.
notin_simpls.
assert (hh:=H0 n Fr).
rewrite <- (@openc_exp_core e0 0 (c_fid n)); auto.
(**)
rewrite H2; auto.
(**)
pick_fresh n.
notin_simpls.
assert (hh:=H0 n Fr).
rewrite <- (@openc_open_exp_core e0 0 (fvar n)); auto.
Qed.


Lemma term_open_exp :
forall e,  term_exp e -> forall k v, open_exp k v e = e.
Proof.
intros e H.
apply termexpind with
(P:= fun e (H: term e) =>
forall k v, open_rec k v e = e)
(P0:= fun e (H: term_exp e) =>
forall k v, open_exp k v e = e)
(P1:= fun v (H: term_val v) =>
forall k v0, open_val k v0 v = v)
(P2:= fun c (H: term_cont c) =>
forall k v, open_cont k v c = c)
(*(forall e L, c = c_lam e -> 
(forall x, x \notin L -> term_exp (open_exp 0 (fvar x) e)) -> 
forall k v, open_cont k v c = c))*)
; intros; subst; simpl; 
try rewrite H0; try rewrite H1; auto.
pick_fresh n.
notin_simpls.
assert (hh:=H0 n Fr).
rewrite <- (@open_openc_exp_core e0 0 (c_fid n)); auto.
(**)
rewrite H2; auto.
(**)
pick_fresh n.
notin_simpls.
assert (hh:=H0 n Fr).
rewrite <- (@open_exp_core e0 0 (fvar n)); auto.
Qed.

Lemma term_open :
forall e,  term e -> forall k v, open_rec k v e = e.
Proof.
intros e H.
apply termind with
(P:= fun e (H: term e) =>
forall k v, open_rec k v e = e)
(P0:= fun e (H: term_exp e) =>
forall k v, open_exp k v e = e)
(P1:= fun v (H: term_val v) =>
forall k v0, open_val k v0 v = v)
(P2:= fun c (H: term_cont c) =>
forall k v, open_cont k v c = c)
(*(forall e L, c = c_lam e -> 
(forall x, x \notin L -> term_exp (open_exp 0 (fvar x) e)) -> 
forall k v, open_cont k v c = c))*)
; intros; subst; simpl; 
try rewrite H0; try rewrite H1; auto.
pick_fresh n.
notin_simpls.
assert (hh:=H0 n Fr).
rewrite <- (@open_openc_exp_core e0 0 (c_fid n)); auto.
(**)
rewrite H2; auto.
(**)
pick_fresh n.
notin_simpls.
assert (hh:=H0 n Fr).
rewrite <- (@open_exp_core e0 0 (fvar n)); auto.
Qed.

Lemma term_val_open :
forall v, term_val v -> forall k v0, open_val k v0 v = v.
Proof.
intros.
inversions H; simpl; auto.
rewrite term_open; auto.
Qed.

Lemma term_val_openc :
forall v, term_val v -> forall k v0, openc_val k v0 v = v.
Proof.
intros.
inversions H; simpl; auto.
rewrite term_openc; auto.
Qed.

Lemma term_cont_openc :
forall c, term_cont c -> forall k v0, openc_cont k v0 c = c.
Proof.
intros c H.
apply termcontind with
(P:= fun e (H: term e) =>
forall k v, openc_rec k v e = e)
(P0:= fun e (H:term_exp e) =>
forall k v, openc_exp k v e = e)
(P1:= fun v (H: term_val v) =>
forall k v0, openc_val k v0 v = v)
(P2:= fun c (H: term_cont c) =>
forall k v, openc_cont k v c = c); intros; subst; simpl; 
try rewrite H0; try rewrite H1; auto.
pick_fresh_for L z.
induction c; try inversions H.
rewrite <- (@openc_exp_core e 0 (c_fid z)); auto.
rewrite H0 with z (S k) v; auto.
rewrite <- (@openc_exp_core e 0 (c_fid z)); auto.
rewrite H0 with z (S k) v; auto.
(**)
rewrite H2; auto.
(**)
pick_fresh n.
notin_simpls.
rewrite <- (@openc_open_exp_core e 0 (fvar n)); auto.
rewrite H0; auto.
Qed.


Lemma substc_exp_openc : forall x u t1 t2, term_cont u -> 
  forall k, substc_exp (openc_exp k t2 t1) x u = 
  openc_exp k (substc_cont t2 x u) (substc_exp t1 x u).
Proof.
  intros x u t1 t2 H. 
  apply trmexpind with
(P:= fun e:trm => forall n, substc (openc_rec n t2 e) x u =
  openc_rec n (substc_cont t2 x u) (substc e x u))
(P0:= fun e:exp => forall n, substc_exp (openc_exp n t2 e) x u =
  openc_exp n (substc_cont t2 x u) (substc_exp e x u))
(P1:= fun v:val => forall n, substc_val (openc_val n t2 v) x u =
  openc_val n (substc_cont t2 x u) (substc_val v x u))
(P2:= fun c:cont => (*forall e, c = c_lam e ->*)
forall n, substc_cont (openc_cont n t2 c) x u =
  openc_cont n (substc_cont t2 x u) (substc_cont c x u)); simpl; intros; auto.
rewrite H0; auto.
(**)
rewrite H0.
rewrite H1; auto.
(**)
rewrite H0.
rewrite H1; auto.
(**)
rewrite H0; rewrite H1; rewrite H2; auto.
(**)
rewrite H0; auto.
rewrite H1; auto.
(**)
rewrite H0; auto.
(**)
case_nat*.
(**)
case_var*.
(**)
Focus 2.
rewrite H0; auto.
rewrite term_cont_openc; auto.
Qed.


Lemma term_cont_open :
forall c, term_cont c -> forall k v0, open_cont k v0 c = c.
Proof.
intros c H.
apply termcontind with
(P:= fun e (H: term e) =>
forall k v, open_rec k v e = e)
(P0:= fun e (H:term_exp e) =>
forall k v, open_exp k v e = e)
(P1:= fun v (H: term_val v) =>
forall k v0, open_val k v0 v = v)
(P2:= fun c (H: term_cont c) =>
forall k v, open_cont k v c = c); intros; subst; simpl; 
try rewrite H0; try rewrite H1; auto.
pick_fresh_for L z.
induction c; try inversions H.
rewrite <- (@open_openc_exp_core e 0 (c_fid z)); auto.
rewrite H0 with z (S k) v; auto.
rewrite <- (@open_openc_exp_core e 0 (c_fid z)); auto.
rewrite H0 with z (S k) v; auto.
(**)
rewrite H2; auto.
(**)
pick_fresh n.
notin_simpls.
rewrite <- (@open_exp_core e 0 (fvar n)); auto.
rewrite H0; auto.
Qed.

Lemma substc_exp_open : forall x u t1 t2, term_cont u -> 
  forall k, substc_exp (open_exp k t2 t1) x u = 
  open_exp k (substc_val t2 x u) (substc_exp t1 x u).
Proof.
  intros x u t1 t2 H. 
  apply trmexpind with
(P:= fun e:trm => forall n, substc (open_rec n t2 e) x u =
  open_rec n (substc_val t2 x u) (substc e x u))
(P0:= fun e:exp => forall n, substc_exp (open_exp n t2 e) x u =
  open_exp n (substc_val t2 x u) (substc_exp e x u))
(P1:= fun v:val => forall n, substc_val (open_val n t2 v) x u =
  open_val n (substc_val t2 x u) (substc_val v x u))
(P2:= fun c:cont => (*forall e, c = c_lam e ->*)
forall n, substc_cont (open_cont n t2 c) x u =
  open_cont n (substc_val t2 x u) (substc_cont c x u)); simpl; intros; auto.
rewrite H0; auto.
(**)
rewrite H0.
rewrite H1; auto.
(**)
rewrite H0.
rewrite H1; auto.
(**)
rewrite H0; rewrite H1; rewrite H2; auto.
(**)
rewrite H0; auto.
rewrite H1; auto.
(**)
case_nat*.
(**)
rewrite H0; auto.
(**)
case_var*.
rewrite term_cont_open; auto.
(**)
rewrite H0; auto.
Qed.

Lemma subst_exp_open : forall x u t1 t2, term_val u -> 
  forall k, subst_exp (open_exp k t2 t1) x u = 
  open_exp k (subst_val t2 x u) (subst_exp t1 x u).
Proof.
  intros x u t1 t2 H. 
  apply trmexpind with
(P:= fun e:trm => forall n, subst (open_rec n t2 e) x u =
  open_rec n (subst_val t2 x u) (subst e x u))
(P0:= fun e:exp => forall n, subst_exp (open_exp n t2 e) x u =
  open_exp n (subst_val t2 x u) (subst_exp e x u))
(P1:= fun v:val => forall n, subst_val (open_val n t2 v) x u =
  open_val n (subst_val t2 x u) (subst_val v x u))
(P2:= fun c:cont => forall e, c = c_lam e ->
forall n, subst_exp (open_exp n t2 e) x u =
  open_exp n (subst_val t2 x u) (subst_exp e x u)); simpl; intros; auto.
rewrite H0; auto.
(**)
induction c; simpl.
rewrite H1; auto.
(**)
rewrite H1; auto.
(**)
rewrite H1; auto.
rewrite H0; auto.
(**)
induction c; simpl; rewrite H0; auto.
rewrite H1; auto.
(**)
induction c; simpls; rewrite H0; auto.
rewrite H1; auto.
rewrite H1; auto.
rewrite H2; auto.
rewrite H1; auto.
(**)
simpl; rewrite H0; auto.
rewrite H1; auto.
(**)
case_nat*.
(**)
case_var*.
rewrite term_val_open; trivial.
(**)
rewrite H0; trivial.
(**)
discriminate.
(**)
discriminate.
(**)
injection H1; intros; subst.
apply H0.
Qed.
 
Lemma subst_openc : forall x u c e, term_val u -> 
  subst_exp (openc_exp 0 c e) x u = openc_exp 0 (subst_cont c x u) (subst_exp e x u).
Proof.
intros. generalize 0.
  apply trmexpind with
(P:= fun e:trm => forall n, subst (openc_rec n c e) x u =
  openc_rec n (subst_cont c x u) (subst e x u))
(P0:= fun e:exp => forall n, subst_exp (openc_exp n c e) x u =
  openc_exp n (subst_cont c x u) (subst_exp e x u))
(P1:= fun v:val => forall n, subst_val (openc_val n c v) x u =
  openc_val n (subst_cont c x u) (subst_val v x u))
(*(P2:= fun c:cont => forall e, c = c_lam e ->
forall n, subst_exp (openc_exp n c e) x u =
  openc_exp n (subst_cont c x u) (subst_exp e x u)); *)
(P2 := fun c':cont => forall n, subst_cont (openc_cont n c c') x u =
  openc_cont n (subst_cont c x u) (subst_cont c' x u));
intros; simpls; f_equal*.
case_var*.
induction c; try inversions H; simpl; auto;
rewrite term_openc; auto.
(**)
case_nat*.
Qed.

Lemma subst_open : forall x u t1 t2, term_val u -> 
  subst (open t1 t2) x u = open (subst t1 x u) (subst_val t2 x u).
Proof.
  intros. unfold open. generalize 0.
  apply trmind with
(P:= fun e:trm => forall n, subst (open_rec n t2 e) x u =
  open_rec n (subst_val t2 x u) (subst e x u))
(P0:= fun e:exp => forall n, subst_exp (open_exp n t2 e) x u =
  open_exp n (subst_val t2 x u) (subst_exp e x u))
(P1:= fun v:val => forall n, subst_val (open_val n t2 v) x u =
  open_val n (subst_val t2 x u) (subst_val v x u))
(P2:= fun c:cont => forall e, c = c_lam e ->
forall n, subst_exp (open_exp n t2 e) x u =
  open_exp n (subst_val t2 x u) (subst_exp e x u)); simpl; intros; auto.
(**)
rewrite H0; auto.
(**)
induction c; simpl.
rewrite H1; auto.
(**)
rewrite H1; auto.
(**)
rewrite H1; auto.
rewrite H0; auto.
(**)
induction c; simpl; rewrite H0; auto.
rewrite H1; auto.
(**)
induction c; simpls; rewrite H0; auto.
rewrite H1; auto.
rewrite H1; auto.
rewrite H2; auto.
rewrite H1; auto.
(**)
rewrite H1; auto.
rewrite H0; auto.
(**)
case_nat*.
(**)
case_var*.
rewrite term_val_open; trivial.
(**)
rewrite H0; trivial.
(**)
discriminate.
(**)
discriminate.
(**)
injection H1; intros; subst.
apply H0.
Qed.
 
Lemma subst_open_var : 
forall x y u e, y <> x -> term_val u ->
  open (subst e x u) (fvar y) = subst (open e (fvar y)) x u.
Proof.
  introv Neq Wu. rewrite* subst_open.
  simpl. case_var*.
Qed.

Lemma subst_exp_open_var : 
forall x y u e, y <> x -> term_val u ->
  forall k, open_exp k (fvar y) (subst_exp e x u) = subst_exp (open_exp k (fvar y) e) x u.
Proof.
  intros x y u e Neq Wu k. rewrite* subst_exp_open.
  simpl. case_var*.
Qed.

Lemma subst_exp_openc : forall x u t1 t2, term_val u -> 
  forall k, subst_exp (openc_exp k t2 t1) x u = 
  openc_exp k (subst_cont t2 x u) (subst_exp t1 x u).
Proof.
  intros x u t1 t2 H. 
  apply trmexpind with
(P:= fun e:trm => forall n, subst (openc_rec n t2 e) x u =
  openc_rec n (subst_cont t2 x u) (subst e x u))
(P0:= fun e:exp => forall n, subst_exp (openc_exp n t2 e) x u =
  openc_exp n (subst_cont t2 x u) (subst_exp e x u))
(P1:= fun v:val => forall n, subst_val (openc_val n t2 v) x u =
  openc_val n (subst_cont t2 x u) (subst_val v x u))
(P2:= fun c:cont => forall e, c = c_lam e ->
forall n, subst_exp (openc_exp n t2 e) x u =
  openc_exp n (subst_cont t2 x u) (subst_exp e x u)); simpl; intros; auto.
rewrite H0; auto.
(**)
induction c; simpl.
case_nat*; simpls.
rewrite H1; auto.
rewrite* H1.
rewrite* H1.
rewrite* H1.
rewrite* H0.
(**)
induction c; simpls.
case_nat*; simpls.
rewrite* H0.
rewrite* H0.
rewrite* H0.
rewrite* H0; rewrite* H1.
(**)
rewrite H1; auto.
rewrite H0; auto.
induction c; simpls.
case_nat*; simpls; rewrite* H2.
auto.
rewrite* H2.
(**)
Focus 3.
rewrite* H0.
(**)
Focus 3.
discriminate.
(**)
Focus 3.
discriminate.
(**)
Focus 3.
injection H1; intros; subst.
rewrite* H0.
(**)
Focus 2.
case_var*.
rewrite* term_val_openc.
(**)
rewrite H1; auto.
rewrite H0; auto.
Qed.
 


Lemma subst_exp_openc_var : 
forall x y u e, y <> x -> term_val u ->
  forall k, openc_exp k (c_fid y) (subst_exp e x u) = subst_exp (openc_exp k (c_fid y) e) x u.
Proof.
  intros x y u e Neq Wu k. rewrite* subst_exp_openc.
Qed.

(** abstracting a variable in a term *)
Fixpoint close_var_rec (k:nat) (x:var) (r:trm) {struct r} : trm :=
match r with
| trm_term e => trm_term (close_var_exp (S k) x e)
end
with
close_var_exp k x e {struct e} : exp :=
match e with
| cont_app c v' => cont_app (close_var_cont k x c) (close_var_val k x v')
| trm_app r c => trm_app (close_var_rec k x r) (close_var_cont k x c)
| val_app v0 v1 c => val_app (close_var_val k x v0) (close_var_val k x v1) (close_var_cont k x c)
| elet z v0 e => elet z (close_var_val k x v0) (close_var_exp k x e)
end
with
close_var_val k x u {struct u} : val :=
match u with
| bvar w => bvar w
| fvar y => if x == y then bvar k else fvar y 
| lam z r => lam z (close_var_rec k x r)
end
with
close_var_cont k x c {struct c} : cont :=
match c with
| c_bid n => c_bid n
| c_fid n => c_fid n (* if n == x then c_bid k else c_fid n *)
| c_lam e => c_lam (close_var_exp (S k) x e)
end.


Definition close_var z t := close_var_rec 0 z t.


Fixpoint closec_var_rec (k:nat) (x:var) (r:trm) {struct r} : trm :=
match r with
| trm_term e => trm_term (closec_var_exp (S k) x e)
end
with
closec_var_exp k x e {struct e} : exp :=
match e with
| cont_app c v' => cont_app (closec_var_cont k x c) (closec_var_val k x v')
| trm_app r c => trm_app (closec_var_rec k x r) (closec_var_cont k x c)
| val_app v0 v1 c => val_app (closec_var_val k x v0) (closec_var_val k x v1) (closec_var_cont k x c)
| elet z v0 e => elet z (closec_var_val k x v0) (closec_var_exp k x e)
end
with
closec_var_val k x u {struct u} : val :=
match u with
| bvar w => bvar w
| fvar y => fvar y 
| lam z r => lam z (closec_var_rec k x r)
end
with
closec_var_cont k x c {struct c} : cont :=
match c with
| c_bid n => c_bid n
| c_fid n => if n == x then c_bid k else c_fid n 
| c_lam e => c_lam (closec_var_exp (S k) x e)
end.

Ltac discr m H1 :=
induction m; unfold open in H1; simpl in H1; try discriminate;
injection H1; intros; subst; clear H1.


Lemma subst_term_cont : forall e z u, term_val u ->
  term_cont e -> term_cont (subst_cont e z u).
Proof.
intros t z u H0 H.
apply termcontind with 
(P:= fun e (H: term e) =>
term (subst e z u))
(P0:= fun e (H:term_exp e) =>
term_exp (subst_exp e z u))
(P1:= fun v (H: term_val v) =>
term_val (subst_val v z u))
(P2:= fun c (H: term_cont c) =>
term_cont (subst_cont c z u)); intros; subst; simpl; repeat constructor; auto; f_equal*.
2: case_var*; constructor.
constructor 1 with L; intros; auto.
replace (c_fid k) with (subst_cont (c_fid k) z u); auto.
rewrite <- subst_openc; auto.
(**)
(*inversions H0.*)
constructor 2 with (L \u {{z}}); intros; auto.
replace (fvar w) with (subst_val (fvar w) z u); auto.
rewrite <- subst_exp_open; auto.
simpl.
case_var*.
(*notin_simpls.
elim H2; auto.*)
Qed.

Lemma subst_term_val : forall e z u, term_val u ->
  term_val e -> term_val (subst_val e z u).
Proof.
intros t z u H0 H.
apply termvalind with 
(P:= fun e (H: term e) =>
term (subst e z u))
(P0:= fun e (H:term_exp e) =>
term_exp (subst_exp e z u))
(P1:= fun v (H: term_val v) =>
term_val (subst_val v z u))
(P2:= fun c (H: term_cont c) =>
term_cont (subst_cont c z u)); intros; subst; simpl; repeat constructor; auto; f_equal*.
2: case_var*; constructor.
constructor 1 with L; intros; auto.
replace (c_fid k) with (subst_cont (c_fid k) z u); auto.
rewrite <- subst_openc; auto.
(**)
(*inversions H0.*)
constructor 2 with (L \u {{z}}); intros; auto.
replace (fvar w) with (subst_val (fvar w) z u); auto.
rewrite <- subst_exp_open; auto.
simpl.
case_var*.
(*notin_simpls.
elim H2; auto.*)
Qed.

Lemma substc_term_exp : forall e z u, term_cont u ->
  term_exp e -> term_exp (substc_exp e z u).
Proof.
intros t z u H0 H.
apply termexpind with 
(P:= fun e (H: term e) =>
term (substc e z u))
(P0:= fun e (H:term_exp e) =>
term_exp (substc_exp e z u))
(P1:= fun v (H: term_val v) =>
term_val (substc_val v z u))
(P2:= fun c (H: term_cont c) =>
term_cont (substc_cont c z u)); intros; subst; simpl; repeat constructor; auto.
2: case_var*; constructor.
Focus 2.
constructor 2 with (L \u {{z}}); auto.
intros.
notin_simpls.
replace (fvar w) with (substc_val (fvar w) z u); auto.
rewrite <- substc_exp_open; auto.
constructor 1 with (L \u {{z}}).
intros.
replace (c_fid k) with (substc_cont (c_fid k) z u).
rewrite <- substc_exp_openc.
apply H1; auto.
auto.
simpls.
case_var*.
(*notin_contradiction.*)
Qed.

Lemma substc_term_val : forall e z u, term_cont u ->
  term_val e -> term_val (substc_val e z u).
Proof.
intros t z u H0 H.
apply termvalind with 
(P:= fun e (H: term e) =>
term (substc e z u))
(P0:= fun e (H:term_exp e) =>
term_exp (substc_exp e z u))
(P1:= fun v (H: term_val v) =>
term_val (substc_val v z u))
(P2:= fun c (H: term_cont c) =>
term_cont (substc_cont c z u)); intros; subst; simpl; repeat constructor; auto.
2: case_var*; constructor.
Focus 2.
constructor 2 with (L \u {{z}}); auto.
intros.
notin_simpls.
replace (fvar w) with (substc_val (fvar w) z u); auto.
rewrite <- substc_exp_open; auto.
constructor 1 with (L \u {{z}}).
intros.
replace (c_fid k) with (substc_cont (c_fid k) z u).
rewrite <- substc_exp_openc.
apply H1; auto.
auto.
simpls.
case_var*.
(*notin_contradiction.*)
Qed.

Lemma substc_term_cont : forall e z u, term_cont u ->
  term_cont e -> term_cont (substc_cont e z u).
Proof.
intros t z u H0 H.
apply termcontind with 
(P:= fun e (H: term e) =>
term (substc e z u))
(P0:= fun e (H:term_exp e) =>
term_exp (substc_exp e z u))
(P1:= fun v (H: term_val v) =>
term_val (substc_val v z u))
(P2:= fun c (H: term_cont c) =>
term_cont (substc_cont c z u)); intros; subst; simpl; repeat constructor; auto.
2: case_var*; constructor.
Focus 2.
constructor 2 with (L \u {{z}}); auto.
intros.
notin_simpls.
replace (fvar w) with (substc_val (fvar w) z u); auto.
rewrite <- substc_exp_open; auto.
constructor 1 with (L \u {{z}}).
intros.
replace (c_fid k) with (substc_cont (c_fid k) z u).
rewrite <- substc_exp_openc.
apply H1; auto.
auto.
simpls.
case_var*.
(*notin_contradiction.*)
Qed.

Lemma subst_term_exp : forall e z u, term_val u ->
  term_exp e -> term_exp (subst_exp e z u).
Proof.
intros t z u H0 H.
apply termexpind with 
(P:= fun e (H: term e) =>
term (subst e z u))
(P0:= fun e (H:term_exp e) =>
term_exp (subst_exp e z u))
(P1:= fun v (H: term_val v) =>
term_val (subst_val v z u))
(P2:= fun c (H: term_cont c) =>
term_cont (subst_cont c z u)); intros; subst; simpl; repeat constructor; auto.
2: case_var*; constructor.
Focus 2.
constructor 2 with (L \u {{z}}); auto.
intros.
notin_simpls.
replace (fvar w) with (subst_val (fvar w) z u); auto.
rewrite <- subst_exp_open; auto.
simpl; auto.
case_var*.
(**)
constructor 1 with (L \u {{z}}); auto.
intros.
replace (c_fid k) with (subst_cont (c_fid k) z u); auto.
rewrite <- subst_openc.
simpl; apply H1; auto.
auto.
Qed.

Lemma subst_term : forall t z u, term_val u ->
  term t -> term (subst t z u).
Proof.
intros t z u H0 H.
apply termind with 
(P:= fun e (H: term e) =>
term (subst e z u))
(P0:= fun e (H:term_exp e) =>
term_exp (subst_exp e z u))
(P1:= fun v (H: term_val v) =>
term_val (subst_val v z u))
(P2:= fun c (H: term_cont c) =>
term_cont (subst_cont c z u)); intros; subst; simpl; repeat constructor; auto.
2: case_var*; constructor.
Focus 2.
constructor 2 with (L \u {{z}}); auto.
intros.
notin_simpls.
replace (fvar w) with (subst_val (fvar w) z u); auto.
rewrite <- subst_exp_open; auto.
simpl; auto.
case_var*.
(**)
constructor 1 with (L \u {{z}}); auto.
intros.
replace (c_fid k) with (subst_cont (c_fid k) z u); auto.
rewrite <- subst_openc.
simpl; apply H1; auto.
auto.
Qed.


Lemma subst_intro : forall x t u, 
  x \notin (fv t) -> term_val u ->
  open t u = subst (open t (fvar x)) x u.
Proof.
  introv Fr Wu. rewrite* subst_open.
  rewrite* subst_fresh.
  simpl.
  case_var*.
Qed.

Lemma subst_exp_intro : forall x e u, 
  x \notin (fv_exp e) -> term_val u ->
  open_exp 0 u e = subst_exp (open_exp 0 (fvar x) e) x u.
Proof.
  introv Fr Wu. rewrite* subst_exp_open.
  rewrite* subst_exp_fresh.
  simpl.
  case_var*.
Qed.

Lemma subst_c_exp_intro : forall x e u, 
  x \notin (fvc_exp e) -> term_cont u ->
  openc_exp 0 u e = substc_exp (openc_exp 0 (c_fid x) e) x u.
Proof.
  introv Fr Wu. rewrite* substc_exp_openc.
  rewrite* substc_exp_fresh.
  replace (substc_cont (c_fid x) x u) with u; auto.
  induction u; simpls; case_var*; auto. 
Qed.

Ltac cross := 
  rewrite subst_open_var; try cross.

Tactic Notation "cross" "*" := 
  cross; auto*.

Definition body e :=
  exists L, forall w, w \notin L -> term_exp (open_exp 0 (fvar w) e).

Definition cbody e :=
  exists L, forall w, w \notin L -> term_exp (openc_exp 0 (c_fid w) e).

Lemma subst_body : forall z u e,
  body e -> term_val u -> body (subst_exp e z u).
Proof.
  unfold body. introv [L H]. exists (L \u {{z}}).
  intros. 
  rewrite~ subst_exp_open_var. use subst_term_exp.
Qed.

Lemma open_term_exp :
forall e v, body e -> term_val v -> term_exp (open_exp 0 v e).
Proof.
  intros. destruct H. pick_fresh y.
  rewrite* (@subst_exp_intro y).
  apply subst_term_exp; auto.
Qed.


Lemma openc_term_exp :
forall e v, cbody e -> term_cont v -> term_exp (openc_exp 0 v e).
Proof.
  intros. destruct H. pick_fresh y.
  rewrite* (@subst_c_exp_intro y).
  apply substc_term_exp; auto.
Qed.

Lemma subset_union_both :
forall A B C D, 
  A << B -> C << D -> A \u C << B \u D.
Proof.
intros.
assert (A << B \u D).
apply subset_trans with B; use subset_union_weak_l.
assert (C << B \u D).
apply subset_trans with D; use subset_union_weak_r.
destruct (@subset_union_l A C (B \u D)).
auto.
Qed.


(*
Lemma fv_subst :
forall e x v,
fv (subst e x v) << fv e \u fv_val v.
Proof.
intro e.
apply trmind with
(P:= fun e =>
forall x v,
fv (subst e x v) << fv e \u fv_val v)
(P0:= fun e =>
forall x v,
fv_exp (subst_exp e x v) << fv_exp e \u fv_val v)
(P1:= fun v0 =>
forall x v,
fv_val (subst_val v0 x v) << fv_val v0 \u fv_val v)
(P2:= fun c =>
forall x v,
fv_cont (subst_cont c x v) << fv_cont c \u fv_val v); intros; subst; simpl; auto.
Focus 4.
apply subset_union_weak_l.
Focus 5.
apply subset_union_weak_l.
Focus 4.
case_var*.
apply subset_union_weak_r.
apply subset_union_weak_l.
(**)
simpl.
assert (hh:=H x v0).
assert (hx:=H0 x v0).
(*
apply subset_union_weak_l.
induction c; simpl; auto.
simpl in H.
assert (hh:=subset_union_l (fv (subst t0 x v)) (fv (subst t x v))
(fv t0 \u fv t \u fv_val v)).
destruct hh.
apply H2; split; auto.
apply subset_trans with (fv t0\u fv_val v); auto.
rewrite <- union_assoc.
rewrite <- union_comm_assoc.
apply subset_union_weak_r.
apply subset_trans with (fv t\u fv_val v); auto.
rewrite <- union_assoc.
apply subset_union_weak_r.
assert (hh:=subset_union_l (fv_val (subst_val v x v1)) (fv_val (subst_val v0 x v1))
(fv_val v \u fv_val v0 \u fv_val v1)).
destruct hh.
apply H2; split; auto.
apply subset_trans with (fv_val v\u fv_val v1); auto.
rewrite <- union_assoc.
rewrite <- union_comm_assoc.
apply subset_union_weak_r.
apply subset_trans with (fv_val v0\u fv_val v1); auto.
rewrite <- union_assoc.
apply subset_union_weak_r.
Qed.
*)
*)

Lemma substc_rd :
forall e0 e1, Rd e0 e1 ->
forall y w, Rd (substc_exp e0 w (c_fid y)) (substc_exp e1 w (c_fid y)).
Proof.
intros e0 e1 H.
induction H; intros; auto.
simpl.
rewrite substc_exp_openc; auto.
constructor 1 with (L \u {{w}}); intros; auto.
replace (c_fid k) with (substc_cont (c_fid k) w (c_fid y)); auto.
rewrite <- substc_exp_openc; auto.
apply substc_term_exp; auto.
constructor.
constructor.
simpls.
case_var*.
(*notin_contradiction.*)
apply substc_term_cont; auto.
constructor.
constructor.
(**)
simpls.
rewrite substc_exp_open; auto.
constructor 2 with (L \u {{w}}); intros.
replace (fvar x) with (substc_val (fvar x) w (c_fid y)); auto.
rewrite <- substc_exp_open; auto.
apply substc_term_exp; auto.
constructor.
constructor.
apply substc_term_val.
constructor.
auto.
constructor.
Qed.

Lemma subst_rd :
forall e0 e1, Rd e0 e1 ->
forall y w, Rd (subst_exp e0 w (fvar y)) (subst_exp e1 w (fvar y)).
Proof.
intros e0 e1 H.
induction H; intros; auto.
simpl.
rewrite subst_openc; auto.
constructor 1 with L; intros; auto.
replace (c_fid k) with (subst_cont (c_fid k) w (fvar y)); auto.
rewrite <- subst_openc; auto.
apply subst_term_exp; auto.
constructor.
constructor.
apply subst_term_cont; auto.
constructor.
constructor.
(**)
simpls.
rewrite subst_exp_open; auto.
constructor 2 with (L \u {{w}}); intros.
replace (fvar x) with (subst_val (fvar x) w (fvar y)); auto.
rewrite <- subst_exp_open; auto.
apply subst_term_exp; auto.
constructor.
constructor.
simpls.
case_var*.
(*notin_contradiction.*)
apply subst_term_val; auto.
constructor.
constructor.
Qed.

(*
Lemma fv_open_exp :
forall e x k, fv_exp (open_exp k (fvar x) e) << fv_exp e \u {{x}}.

Lemma fv_open :
forall e x k, fv (open_rec k (fvar x) e) << fv e \u {{x}}.
Proof.
intro e.
apply trmind with
(P:= fun e =>
forall x k,
fv (open_rec k (fvar x) e) << fv e \u {{x}})
(P0:= fun e =>
forall x k,
fv_exp (open_exp k (fvar x) e) << fv_exp e \u {{x}})
(P1:= fun v =>
forall x k,
fv_val (open_val k (fvar x) v) << fv_val v \u {{x}})
(P2:= fun c =>
forall x k,
fv_cont (open_cont k (fvar x) c) << fv_cont c \u {{x}}); 
simpl; intros; f_equal*. 
Focus 4.
case_nat*; simpl; auto.
apply subset_union_weak_r.
rewrite union_empty_l; apply subset_empty_l.

Lemma fv_open_val :
forall e v k, fv (open_rec k v e) << fv e \u fv_val v.
Proof.
intro e.
apply trmind with
(P:= fun e =>
forall x k,
fv (open_rec k x e) << fv e \u fv_val x)
(P0:= fun v =>
forall x k,
fv_val (open_val k x v) << fv_val v \u fv_val x)
(P1:= fun c =>
forall x k,
fv_cont (open_let k x c) << fv_cont c \u fv_val x); 
intros; subst; auto.
Focus 3.
assert (hh:=subset_union_l (fv_val (open_val k x v))
(fv_val (open_val k x v0))
(fv_val v \u fv_val v0 \u fv_val x)).
destruct hh.
apply H2; split; auto.
apply subset_trans with (fv_val v\u fv_val x); auto.
rewrite <- union_assoc.
rewrite <- union_comm_assoc.
apply subset_union_weak_r.
apply subset_trans with (fv_val v0\u fv_val x); auto.
rewrite <- union_assoc.
apply subset_union_weak_r.
Focus 4.
simpl.
apply subset_union_weak_l.
Focus 4.
simpl.
apply subset_union_weak_l.
Focus 3.
induction n; simpl.
induction k; simpl.
apply subset_union_weak_r.
apply subset_union_weak_l.
simpl in IHn.
elim (k===S n); intros; auto.
simpl.
apply subset_union_weak_r.
simpl.
apply subset_union_weak_l.
simpl; auto.
induction c; unfold open; simpl; auto.
simpl in H.
assert (hh:=subset_union_l (fv (open_rec (k+1) x t0)) 
(fv (open_rec k x t))
(fv t0 \u fv t \u fv_val x)).
destruct hh.
apply H2; split; auto.
apply subset_trans with (fv t0\u fv_val x); auto.
rewrite <- union_assoc.
rewrite <- union_comm_assoc.
apply subset_union_weak_r.
apply subset_trans with (fv t\u fv_val x); auto.
rewrite <- union_assoc.
apply subset_union_weak_r.
simpl; auto.
simpl; auto.
Qed.
*)

Lemma let_cont_body : forall e, 
  term_cont (c_lam e) -> body e.
Proof.
  intros. unfold body. inversion* H.
Qed.

Lemma body_let_cont : forall e, 
  body e -> term_cont (c_lam e).
Proof.
  intros. inversion* H.
  econstructor; eauto.
Qed.

Hint Resolve let_cont_body body_let_cont.

Lemma openc_exp_var_inj : forall x e1 e2, 
  x \notin (fv_exp e1) -> x \notin (fvc_exp e1) -> x \notin (fvc_exp e2)  -> x \notin (fv_exp e2) -> 
  (openc_exp 0 (c_fid x) e1 = openc_exp 0 (c_fid x) e2) -> (e1 = e2).
Proof.
  intros x t1. generalize 0.
eapply trmexpind with
(P:= fun t1 => forall n t2, x \notin fv t1 -> x \notin (fvc t1) -> x \notin (fvc t2)  -> 
 x \notin fv t2 -> openc_rec n (c_fid x) t1 = openc_rec n (c_fid x) t2 -> t1 = t2)
(P0:= fun t1 => forall n t2, x \notin fv_exp t1 -> x \notin (fvc_exp t1) -> x \notin (fvc_exp t2)  -> 
 x \notin fv_exp t2 -> openc_exp n (c_fid x) t1 = openc_exp n (c_fid x) t2 -> t1 = t2)
(P1:= fun v1 => forall n t2, x \notin fv_val v1 -> x \notin (fvc_val v1) -> x \notin (fvc_val t2)  -> 
 x \notin fv_val t2 -> openc_val n (c_fid x) v1 = openc_val n (c_fid x) t2 -> v1 = t2)
(P2:= fun c => forall n t2, x \notin fv_cont c -> x \notin (fvc_cont c) -> x \notin (fvc_cont t2)  -> 
 x \notin fv_cont t2 -> openc_cont n (c_fid x) c = openc_cont n (c_fid x) t2 -> c = t2); 
intros; subst; simpls; notin_simpls; try (eapply H; eauto); auto.
induction t2; simpls.
f_equal*.
injection H4; intros; eapply H; eauto.
(**)
induction t2; simpls; try discriminate.
injection H5; intros; auto.
f_equal*.
(**)
induction t2; simpls; try discriminate.
injection H5; intros; f_equal*.
(**)
induction t2; simpls; try discriminate.
injection H6; intros; f_equal*.
(**)
induction t2; simpls; try discriminate; auto.
injection H5; intros; f_equal*.
(**)
induction t2; simpls; try discriminate; auto.
(**)
induction t2; simpls; try discriminate; auto.
(**)
induction t2; simpls; try discriminate; auto.
injection H4; intros; f_equal*.
(**)
case_nat*; induction t2; simpls; try discriminate.
case_nat*; try discriminate.
injection H3; intros; subst.
destruct (notin_singleton k k).
elim (H H1).
trivial.
case_nat*.
discriminate.
induction t2; simpls; try discriminate; auto.
case_nat*.
injection H3; intros; subst; elim H; auto.
(**)
induction t2; simpls; try discriminate.
case_nat*; try discriminate.
injection H4; intros; auto.
f_equal*; auto.
Qed.



(*
Lemma openc_exp_var_inj : forall x e1 e2, 
  x \notin (fv_exp e1) -> x \notin (fv_exp e2) -> 
  (openc_exp 0 (c_fid x) e1 = openc_exp 0 (c_fid x) e2) -> (e1 = e2).
Proof.
  intros x t1. generalize 0.
eapply trmexpind with
(P:= fun t1 => forall n t2, x \notin fv t1 ->
 x \notin fv t2 -> openc_rec n (c_fid x) t1 = openc_rec n (c_fid x) t2 -> t1 = t2)
(P0:= fun t1 => forall n t2, x \notin fv_exp t1 ->
 x \notin fv_exp t2 -> openc_exp n (c_fid x) t1 = openc_exp n (c_fid x) t2 -> t1 = t2)
(P1:= fun v1 => forall n t2, x \notin fv_val v1 ->
 x \notin fv_val t2 -> openc_val n (c_fid x) v1 = openc_val n (c_fid x) t2 -> v1 = t2)
(P2:= fun c => forall n t2, x \notin fv_cont c ->
 x \notin fv_cont t2 -> openc_cont n (c_fid x) c = openc_cont n (c_fid x) t2 -> c = t2); 
intros; subst; simpls; notin_simpls; try (eapply H; eauto); auto.
induction t2; simpls.
f_equal*.
injection H2; intros; eapply H; eauto.
(**)
induction t2; simpls; try discriminate.
injection H3; intros; auto.
injection H4; intros; f_equal*.
(**)
induction t2; simpls; try discriminate.
injection H3; intros; f_equal*.
(**)
induction t2; simpls; try discriminate.
injection H4; intros; f_equal*.
(**)
induction t2; simpls; try discriminate; auto.
(**)
induction t2; simpls; try discriminate; auto.
(**)
induction t2; simpls; try discriminate; auto.
injection H2; intros; f_equal*.
(**)
case_nat*; induction t2; simpls; try discriminate.
case_nat*; try discriminate.
injection H1; intros; subst; notin_contradiction.
case_nat*.
discriminate.
induction t2; simpls; try discriminate; auto.
case_nat*.
injection H1; intros; subst; elim H2; auto.
(**)
induction t2; simpls; try discriminate.
case_nat*; try discriminate.
injection H2; intros; auto.
f_equal*; auto.
Qed.
*)

Lemma open_exp_var_inj : forall x e1 e2, 
  x \notin (fv_exp e1) -> x \notin (fv_exp e2) -> 
  (open_exp 0 (fvar x) e1 = open_exp 0 (fvar x) e2) -> (e1 = e2).
Proof.
  intros x t1. unfold open. generalize 0.
eapply trmexpind with
(P:= fun t1 => forall n t2, x \notin fv t1 ->
 x \notin fv t2 -> open_rec n (fvar x) t1 = open_rec n (fvar x) t2 -> t1 = t2)
(P0:= fun t1 => forall n t2, x \notin fv_exp t1 ->
 x \notin fv_exp t2 -> open_exp n (fvar x) t1 = open_exp n (fvar x) t2 -> t1 = t2)
(P1:= fun v1 => forall n t2, x \notin fv_val v1 ->
 x \notin fv_val t2 -> open_val n (fvar x) v1 = open_val n (fvar x) t2 -> v1 = t2)
(P2:= fun c => forall n t2, x \notin fv_cont c ->
 x \notin fv_cont t2 -> open_cont n (fvar x) c = open_cont n (fvar x) t2 -> c = t2); 
intros; subst; simpls; try (eapply H; eauto); auto.
induction t2; simpls.
f_equal*.
injection H2; intros; eapply H; eauto.
(**)
induction t2; simpls; try discriminate.
injection H3; intros; auto.
f_equal*; auto.
(**)
induction t2; simpls; try discriminate.
injection H3; intros; f_equal*.
(**)
induction t2; simpls; try discriminate.
injection H4; intros; f_equal*.
(**)
Focus 4.
induction t2; simpls; try discriminate.
case_nat*.
discriminate.
discriminate.
injection H2; intros; auto.
f_equal*; auto.
(**)
Focus 6.
induction t2; simpls; try discriminate.
injection H2; intros; auto.
f_equal*; auto.
(**)
Focus 5.
induction t2; simpls; try discriminate; auto.
(**)
Focus 4.
induction t2; simpls; try discriminate; auto.
(**)
Focus 3.
induction t2; simpls; try discriminate; auto.
case_nat*.
injection H1; intros; subst.
destruct (notin_singleton x x).
elim (H2 H); trivial.
(*; notin_contradiction.*)
(**)
Focus 2.
case_nat*.
induction t2; simpls; intros; try discriminate; auto.
case_nat*.
Focus 2.
injection H1; intros; subst.
destruct (notin_singleton v v).
elim (H2 H0); trivial.
(*; notin_contradiction.*)
Focus 3.
induction t2; simpls; intros; try discriminate; auto.
case_nat*.
discriminate.
Focus 2.
discriminate.
(**)
induction t2; simpls; try discriminate; auto.
injection H3; intros; auto.
f_equal*; auto.
Qed.

Lemma open_var_inj : forall x t1 t2, 
  x \notin (fv t1) -> x \notin (fv t2) -> 
  (open t1 (fvar x) = open t2 (fvar x)) -> (t1 = t2).
Proof.
  intros x t1. unfold open. generalize 0.
eapply trmind with
(P:= fun t1 => forall n t2, x \notin fv t1 ->
 x \notin fv t2 -> open_rec n (fvar x) t1 = open_rec n (fvar x) t2 -> t1 = t2)
(P0:= fun t1 => forall n t2, x \notin fv_exp t1 ->
 x \notin fv_exp t2 -> open_exp n (fvar x) t1 = open_exp n (fvar x) t2 -> t1 = t2)
(P1:= fun v1 => forall n t2, x \notin fv_val v1 ->
 x \notin fv_val t2 -> open_val n (fvar x) v1 = open_val n (fvar x) t2 -> v1 = t2)
(P2:= fun c => forall n t2, x \notin fv_cont c ->
 x \notin fv_cont t2 -> open_cont n (fvar x) c = open_cont n (fvar x) t2 -> c = t2); 
intros; subst; simpls; try (eapply H; eauto); auto.
induction t2; simpls.
f_equal*.
injection H2; intros; eapply H; eauto.
(**)
induction t2; simpls; try discriminate.
injection H3; intros; auto.
f_equal*; auto.
(**)
induction t2; simpls; try discriminate.
injection H3; intros; f_equal*.
(**)
induction t2; simpls; try discriminate.
injection H4; intros; f_equal*.
(**)
induction t2; simpls; try discriminate.
injection H3; intros; f_equal*.
(**)
Focus 3.
induction t2; simpls; try discriminate.
case_nat*.
discriminate.
discriminate.
injection H2; intros; auto.
f_equal*; auto.
(**)
Focus 5.
induction t2; simpls; try discriminate.
injection H2; intros; auto.
f_equal*; auto.
(**)
Focus 4.
induction t2; simpls; try discriminate; auto.
(**)
Focus 3.
induction t2; simpls; try discriminate; auto.
(**)
Focus 2.
induction t2; simpls; try discriminate; auto.
case_nat*.
injection H1; intros; subst.
destruct (notin_singleton x x).
elim (H2 H); trivial.
(*notin_contradiction.*)
(**)
case_nat*.
induction t2; simpls; intros; try discriminate; auto.
case_nat*.
Focus 2.
injection H1; intros; subst.
destruct (notin_singleton v v).
elim (H2 H0); trivial.
(*; notin_contradiction.*)
Focus 2.
induction t2; simpls; intros; try discriminate; auto.
case_nat*.
discriminate.
discriminate.
Qed.

Lemma close_var_rec_open_exp : forall x y z t1 i j,
  i <> j -> y <> x -> y \notin (fv_exp t1) ->
    open_exp i (fvar y) (open_exp j (fvar z) (close_var_exp j x t1)) 
  = open_exp j (fvar z) (close_var_exp j x (open_exp i (fvar y) t1)).
Proof.
intros x y z t1.
apply trmexpind with
(P:= fun t1 =>
forall i j, i<>j  -> y<>x -> y \notin (fv t1) ->
open_rec i (fvar y) (open_rec j (fvar z) (close_var_rec j x t1)) 
= open_rec j (fvar z) (close_var_rec j x (open_rec i (fvar y) t1)))
(P0:= fun t1 =>
forall i j, i<>j  -> y<>x -> y \notin (fv_exp t1) ->
open_exp i (fvar y) (open_exp j (fvar z) (close_var_exp j x t1)) 
= open_exp j (fvar z) (close_var_exp j x (open_exp i (fvar y) t1)))
(P1:= fun v =>
forall i j, i<>j  -> y<>x -> y \notin (fv_val v) ->
open_val i (fvar y) (open_val j (fvar z) (close_var_val j x v)) 
= open_val j (fvar z) (close_var_val j x (open_val i (fvar y) v)))
(P2:= fun c =>
forall i j, i<>j  -> y<>x -> y \notin (fv_cont c) ->
open_cont i (fvar y) (open_cont j (fvar z) (close_var_cont j x c)) 
= open_cont j (fvar z) (close_var_cont j x (open_cont i (fvar y) c)));
intros; simpls; try solve [ f_equal* ].
case_nat*; auto.
case_nat*; auto.
simpl.
case_nat*.
repeat case_nat*.
simpl.
case_nat*.
case_var*.
simpl.
repeat case_nat*.
case_var*; simpl.
case_nat*.
Qed.

Lemma close_var_rec_open : forall x y z t1 i j,
  i <> j -> y <> x -> y \notin (fv t1) ->
    open_rec i (fvar y) (open_rec j (fvar z) (close_var_rec j x t1)) 
  = open_rec j (fvar z) (close_var_rec j x (open_rec i (fvar y) t1)).
Proof.
intros x y z t1.
apply trmind with
(P:= fun t1 =>
forall i j, i<>j  -> y<>x -> y \notin (fv t1) ->
open_rec i (fvar y) (open_rec j (fvar z) (close_var_rec j x t1)) 
= open_rec j (fvar z) (close_var_rec j x (open_rec i (fvar y) t1)))
(P0:= fun t1 =>
forall i j, i<>j  -> y<>x -> y \notin (fv_exp t1) ->
open_exp i (fvar y) (open_exp j (fvar z) (close_var_exp j x t1)) 
= open_exp j (fvar z) (close_var_exp j x (open_exp i (fvar y) t1)))
(P1:= fun v =>
forall i j, i<>j  -> y<>x -> y \notin (fv_val v) ->
open_val i (fvar y) (open_val j (fvar z) (close_var_val j x v)) 
= open_val j (fvar z) (close_var_val j x (open_val i (fvar y) v)))
(P2:= fun c =>
forall i j, i<>j  -> y<>x -> y \notin (fv_cont c) ->
open_cont i (fvar y) (open_cont j (fvar z) (close_var_cont j x c)) 
= open_cont j (fvar z) (close_var_cont j x (open_cont i (fvar y) c)));
intros; simpls; try solve [ f_equal* ].
case_nat*; auto.
case_nat*; auto.
simpl.
case_nat*.
repeat case_nat*.
simpl.
case_nat*.
case_var*.
simpl.
repeat case_nat*.
case_var*; simpl.
case_nat*.
Qed.


Lemma close_var_rec_openc_open_exp : forall x y z t1 i j,
  i <> j -> y <> x -> y \notin (fv_exp t1) ->
    openc_exp i (c_fid y) (open_exp j (fvar z) (close_var_exp j x t1)) 
  = open_exp j (fvar z) (close_var_exp j x (openc_exp i (c_fid y) t1)).
Proof.
intros x y z t1.
apply trmexpind with
(P:= fun t1 =>
forall i j, i<>j  -> y<>x -> y \notin (fv t1) ->
openc_rec i (c_fid y) (open_rec j (fvar z) (close_var_rec j x t1)) 
= open_rec j (fvar z) (close_var_rec j x (openc_rec i (c_fid y) t1)))
(P0:= fun t1 =>
forall i j, i<>j  -> y<>x -> y \notin (fv_exp t1) ->
openc_exp i (c_fid y) (open_exp j (fvar z) (close_var_exp j x t1)) 
= open_exp j (fvar z) (close_var_exp j x (openc_exp i (c_fid y) t1)))
(P1:= fun v =>
forall i j, i<>j  -> y<>x -> y \notin (fv_val v) ->
openc_val i (c_fid y) (open_val j (fvar z) (close_var_val j x v)) 
= open_val j (fvar z) (close_var_val j x (openc_val i (c_fid y) v)))
(P2:= fun c =>
forall i j, i<>j  -> y<>x -> y \notin (fv_cont c) ->
openc_cont i (c_fid y) (open_cont j (fvar z) (close_var_cont j x c)) 
= open_cont j (fvar z) (close_var_cont j x (openc_cont i (c_fid y) c)));
intros; simpls; try solve [ f_equal* ].
case_nat*; auto.
case_var*; auto.
simpl.
case_nat*.
repeat case_nat*.
Qed.

(*
Lemma in_subset :
forall E F x,
E << F -> x \in E -> x \in F.
Proof.
intros.
destruct (subset_singleton x F).
apply H2.
apply subset_trans with E; auto.
destruct (subset_singleton x E); auto.
Qed.

Lemma fv_close_var_exp :
forall e k x,
fv_exp (close_var_exp k x e) << fv_exp e \u {{x}}.


Lemma fv_close_var :
forall e k x,
fv (close_var_rec k x e) << fv e \u {{x}}.
Proof.
intro e.
apply trmind with
(P:= fun e =>
forall k x,
fv (close_var_rec k x e) << fv e \u {{x}})
(P0:= fun e =>
forall k x,
fv_exp (close_var_exp k x e) << fv_exp e \u {{x}})
(P1:= fun v =>
forall k x,
fv_val (close_var_val k x v) << fv_val v \u {{x}})
(P2:= fun c =>
forall k x,
fv_cont (close_var_cont k x c) << fv_cont c \u {{x}});
intros; subst; simpl; auto.
*)

Lemma close_var_open_id_exp : forall x t,
  term_exp t -> t = open_exp 0 (fvar x) (close_var_exp 0 x t).
Proof.
introv W. unfold close_var. generalize 0.
apply termexpind with
(P:= fun t (H:term t) => forall n, t = open_rec n (fvar x) (close_var_rec n x t))
(P0:= fun t (H:term_exp t) => forall n, t = open_exp n (fvar x) (close_var_exp n x t))
(P1:= fun t (H:term_val t) => forall n, t = open_val n (fvar x) (close_var_val n x t))
(P2:= fun t (H:term_cont t) => 
forall n, t = open_cont n (fvar x) (close_var_cont n x t)); 
simpl; intros; try solve [ f_equal* ].
Focus 2.
case_var*; simpl.
case_nat*.
(**)
pick_fresh_for (L \u {{x}} \u (fv_exp e) \u (fvc_exp e) \u 
(fv_exp (open_exp (S n) (fvar x) (close_var_exp (S n) x e))) \u 
(fvc_exp (open_exp (S n) (fvar x) (close_var_exp (S n) x e)))) z.
notin_simpls.
f_equal*.
apply openc_exp_var_inj with z; auto.
assert (hh:=H z Fr0 (S n)).
rewrite <- close_var_rec_openc_open_exp in hh; auto.
(**)
pick_fresh_for (L \u {{x}} \u (fv_exp e) \u (fvc_exp e) \u 
(fv_exp (open_exp (S n) (fvar x) (close_var_exp (S n) x e))) \u 
(fvc_exp (open_exp (S n) (fvar x) (close_var_exp (S n) x e)))) z.
notin_simpls.
f_equal*.
apply open_exp_var_inj with z; auto.
assert (hh:=H z Fr0 (S n)).
rewrite <- close_var_rec_open_exp in hh; auto.
Qed.

Lemma close_var_open_id : forall x t,
  term t -> t = open (close_var x t) (fvar x).
Proof.
introv W. unfold close_var, open. generalize 0.
apply termind with
(P:= fun t (H:term t) => forall n, t = open_rec n (fvar x) (close_var_rec n x t))
(P0:= fun t (H:term_exp t) => forall n, t = open_exp n (fvar x) (close_var_exp n x t))
(P1:= fun t (H:term_val t) => forall n, t = open_val n (fvar x) (close_var_val n x t))
(P2:= fun t (H:term_cont t) => 
forall n, t = open_cont n (fvar x) (close_var_cont n x t)); 
simpl; intros; try solve [ f_equal* ].
Focus 2.
case_var*; simpl.
case_nat*.
(**)
pick_fresh_for (L \u {{x}} \u (fv_exp e) \u (fvc_exp e) \u 
(fv_exp (open_exp (S n) (fvar x) (close_var_exp (S n) x e))) \u 
(fvc_exp (open_exp (S n) (fvar x) (close_var_exp (S n) x e)))) z.
notin_simpls.
f_equal*.
apply openc_exp_var_inj with z; auto.
assert (hh:=H z Fr0 (S n)).
rewrite <- close_var_rec_openc_open_exp in hh; auto.
(**)
pick_fresh_for (L \u {{x}} \u (fv_exp e) \u (fvc_exp e) \u 
(fv_exp (open_exp (S n) (fvar x) (close_var_exp (S n) x e))) \u 
(fvc_exp (open_exp (S n) (fvar x) (close_var_exp (S n) x e)))) z.
notin_simpls.
f_equal*.
apply open_exp_var_inj with z; auto.
assert (hh:=H z Fr0 (S n)).
rewrite <- close_var_rec_open_exp in hh; auto.
Qed.


Lemma close_var_body : forall x t,
  term_exp t -> body (close_var_exp 0 x t).
Proof.
introv W. exists {{x}}. intros y Fr.
unfold open, close_var. generalize 0. gen y.
apply termexpind with
(P:= fun t (H:term t) =>
forall y, y \notin {{x}} -> forall n,
term (open_rec n (fvar y) (close_var_rec n x t)))
(P0:= fun t (H:term_exp t) =>
forall y, y \notin {{x}} -> forall n,
term_exp (open_exp n (fvar y) (close_var_exp n x t)))
(P1:= fun v (H:term_val v) =>
forall y, y \notin {{x}} -> forall n,
term_val (open_val n (fvar y) (close_var_val n x v)))
(P2:= fun c (H:term_cont c) =>
forall y, y \notin {{x}} -> forall n,
term_cont (open_cont n (fvar y) (close_var_cont n x c)));
intros; subst; simpl; auto.
constructor 1 with (L \u fv_exp e \u {{x}} \u {{y}}); intros; auto.
rewrite* close_var_rec_openc_open_exp.
(**)
constructor; auto.
(**)
constructor; auto.
(**)
constructor; auto.
(**)
constructor; auto.
(**)
case_var*; simpl; auto.
case_nat*; constructor.
constructor.
(**)
constructor; auto.
(**)
constructor; auto.
(**)
simpl.
constructor 2 with (L \u (fv_exp e) \u {{x}}); auto.
intros.
notin_simpl_hyps.
rewrite* close_var_rec_open_exp.
Qed.

Lemma close_var_fresh : forall x t,
  x \notin fv (close_var x t).
Proof.
introv. unfold close_var. generalize 0.
apply trmind with
(P:= fun t =>
forall n, x \notin fv (close_var_rec n x t))
(P0:= fun t =>
forall n, x \notin fv_exp (close_var_exp n x t))
(P1:= fun v =>
forall n, x \notin fv_val (close_var_val n x v))
(P2:= fun c => (*(forall e, c = c_lam e ->
forall n, x \notin fv_exp (close_var_exp n x e)) /\ *) 
(forall n, x \notin fv_cont (close_var_cont n x c))); intros; 
simpl; notin_simpl; simpls*; auto.
case_var*; simpls*.
Qed.

Lemma close_var_fresh_exp : forall x t,
  x \notin fv_exp (close_var_exp 0 x t).
Proof.
intros x t. generalize 0.
apply trmexpind with
(P:= fun t =>
forall n, x \notin fv (close_var_rec n x t))
(P0:= fun t =>
forall n, x \notin fv_exp (close_var_exp n x t))
(P1:= fun v =>
forall n, x \notin fv_val (close_var_val n x v))
(P2:= fun c => (*(forall e, c = c_lam e ->
forall n, x \notin fv_exp (close_var_exp n x e)) /\ *) 
(forall n, x \notin fv_cont (close_var_cont n x c))); intros; 
simpl; notin_simpl; simpls*; try inversions H0; auto.
case_var*.
simpl; auto.
simpl; auto.
Qed.



Lemma close_var_spec : forall e x, term_exp e -> 
  exists u, e = open_exp 0 (fvar x) u /\ body u /\ x \notin (fv_exp u).
Proof.
  intros. exists (close_var_exp 0 x e). split3.
  apply* close_var_open_id_exp.
  trivial. 
  apply* close_var_body.
  trivial.
  apply* close_var_fresh_exp.
Qed.

Lemma close_var_spec_inf : forall e x, term_exp e -> 
  {u : exp | e = open_exp 0 (fvar x) u /\ body u /\ x \notin (fv_exp u)}.
Proof.
  intros. exists (close_var_exp 0 x e). split3.
  apply* close_var_open_id_exp; trivial.
  apply* close_var_body; trivial.
  apply* close_var_fresh_exp.
Qed.

(*
Lemma fv_open_subset :
forall (e:trm) x, 
fv e << fv (open e (fvar x)).
Proof.
intro e.
unfold open.
generalize 0.
apply trmind with
(P:= fun e =>
forall n x, 
fv e << fv (open_rec n (fvar x) e))
(P0:= fun e =>
forall n x,
fv_exp e << fv_exp (open_exp n (fvar x) e))
(P1:= fun e =>
forall n x, 
fv_val e << fv_val (open_val n (fvar x) e))
(P2:= fun e =>
forall n x, 
fv_cont e << fv_cont (open_cont n (fvar x) e));
simpl; intros; subst; auto.
*)

Lemma close_var_open_exp :
forall e x y k, (forall x, open_exp k (fvar x) e = e) ->
open_exp k (fvar x) (close_var_exp k y e) = subst_exp e y (fvar x).
Proof.
intros e.
apply trmexpind with
(P:= fun e =>
forall x y n, (forall x, open_rec n (fvar x) e = e) ->
open_rec n (fvar x) (close_var_rec n y e) = subst e y (fvar x))
(P0:= fun e =>
forall x y n, (forall x, open_exp n (fvar x) e = e) ->
open_exp n (fvar x) (close_var_exp n y e) = subst_exp e y (fvar x))
(P1:= fun v =>
forall x y n, (forall x, open_val n (fvar x) v = v) ->
open_val n (fvar x) (close_var_val n y v) = subst_val v y (fvar x))
(P2:= fun c =>
forall x y n, (forall x, open_cont n (fvar x) c = c) ->
open_cont n (fvar x) (close_var_cont n y c) = subst_cont c y (fvar x)); simpl; intros; subst; auto.
Focus 7.
replace (S n) with (n+1).
rewrite H; auto.
intros.
assert (hh:=H0 x0).
injection hh; intros; auto.
intuition.
(**)
rewrite H; auto.
intros.
assert (hh:=H0 x0).
injection hh; intros; auto.
(**)
rewrite H; auto.
rewrite H0; auto.
induction c; simpls.
intros.
assert (hh:=H1 x0).
injection hh; intros; auto.
intros.
assert (hh:=H1 x0).
injection hh; intros; auto.
simpls.
intros.
(**)
Focus 6.
case_var*; simpl.
case_nat*.
(**)
Focus 6.
rewrite H; auto.
intros; f_equal*.
assert (hh:= H0 x0).
injection hh; intros.
auto.
(**)
Focus 4.
rewrite H; auto.
rewrite H0; auto.
rewrite H1; auto.
intros.
assert (hh:=H2 x0).
injection hh; intros; auto.
intros.
assert (hh:=H2 x0).
injection hh; intros; auto.
intros.
assert (hh:=H2 x0).
injection hh; intros; auto.
(**)
Focus 3.
rewrite H; auto.
rewrite H0; auto.
intros.
assert (hh:=H1 x0).
injection hh; intros; auto.
intros.
assert (hh:=H1 x0).
injection hh; intros; auto.
(**)
Focus 2.
intros.
assert (hh:=H1 x0).
injection hh; intros; auto.
assert (hh:=H1 x0).
injection hh; intros; auto.
(**)
rewrite H0; auto.
rewrite H; auto.
intros.
assert (hh:=H1 x0).
injection hh; intros; auto.
intros.
assert (hh:=H1 x0).
injection hh; intros; auto.
Qed.


Lemma closec_var_openc_exp :
forall e x y k, (forall x, openc_exp k (c_fid x) e = e) ->
openc_exp k (c_fid x) (closec_var_exp k y e) = substc_exp e y (c_fid x).
Proof.
intros e.
apply trmexpind with
(P:= fun e =>
forall x y n, (forall x, openc_rec n (c_fid x) e = e) ->
openc_rec n (c_fid x) (closec_var_rec n y e) = substc e y (c_fid x))
(P0:= fun e =>
forall x y n, (forall x, openc_exp n (c_fid x) e = e) ->
openc_exp n (c_fid x) (closec_var_exp n y e) = substc_exp e y (c_fid x))
(P1:= fun v =>
forall x y n, (forall x, openc_val n (c_fid x) v = v) ->
openc_val n (c_fid x) (closec_var_val n y v) = substc_val v y (c_fid x))
(P2:= fun c =>
forall x y n, (forall x, openc_cont n (c_fid x) c = c) ->
openc_cont n (c_fid x) (closec_var_cont n y c) = substc_cont c y (c_fid x)); simpl; intros; subst; auto.
rewrite H; auto.
intros.
assert (hh:=H0 x0).
injection hh; intros; auto.
(**)
Focus 4.
rewrite H; auto.
rewrite H0; auto.
intros.
assert (hh:=H1 x0).
injection hh; auto.
intros.
assert (hh:=H1 x0).
injection hh; auto.
(**)
Focus 4.
rewrite H; auto.
intros.
assert (hh:=H0 x0).
injection hh; intros; auto.
(**)
Focus 4.
case_var*.
simpls.
case_nat*.
(**)
Focus 4.
rewrite H; auto.
intros.
assert (hh:=H0 x0).
injection hh; subst; auto.
(**)
Focus 3.
rewrite H0.
rewrite H1.
rewrite H.
auto.
intros.
assert (hh:=H2 x0).
injection hh; intros.
auto.
intros.
assert (hh:=H2 x0).
injection hh; intros.
auto.
intros.
assert (hh:=H2 x0).
injection hh; intros.
auto.
(**)
Focus 2.
rewrite H.
rewrite H0.
auto.
intros.
assert (hh:=H1 x0).
injection hh; intros; auto.
intros.
assert (hh:=H1 x0).
injection hh; intros; auto.
(**)
rewrite H0.
rewrite H.
auto.
intros.
assert (hh:=H1 x0).
injection hh; intros; auto.
intros.
assert (hh:=H1 x0).
injection hh; intros; auto.
Qed.


Lemma close_var_open :
forall e x y k, (forall x, open_rec k (fvar x) e = e) ->
open_rec k (fvar x) (close_var_rec k y e) = subst e y (fvar x).
Proof.
intros e.
apply trmind with
(P:= fun e =>
forall x y n, (forall x, open_rec n (fvar x) e = e) ->
open_rec n (fvar x) (close_var_rec n y e) = subst e y (fvar x))
(P0:= fun e =>
forall x y n, (forall x, open_exp n (fvar x) e = e) ->
open_exp n (fvar x) (close_var_exp n y e) = subst_exp e y (fvar x))
(P1:= fun v =>
forall x y n, (forall x, open_val n (fvar x) v = v) ->
open_val n (fvar x) (close_var_val n y v) = subst_val v y (fvar x))
(P2:= fun c =>
forall x y n, (forall x, open_cont n (fvar x) c = c) ->
open_cont n (fvar x) (close_var_cont n y c) = subst_cont c y (fvar x)); simpl; intros; subst; auto.
Focus 5.
rewrite H; auto.
rewrite H0; auto.
intros.
assert (hh:=H1 x0).
injection hh; intros; auto.
intros.
assert (hh:=H1 x0).
injection hh; intros; auto.
(**)
Focus 6.
replace (S n) with (n+1).
rewrite H; auto.
intros.
assert (hh:=H0 x0).
injection hh; intros; auto.
intuition.
(**)
rewrite H; auto.
intros.
assert (hh:=H0 x0).
injection hh; intros; auto.
(**)
rewrite H; auto.
rewrite H0; auto.
induction c; simpls.
intros.
assert (hh:=H1 x0).
injection hh; intros; auto.
intros.
assert (hh:=H1 x0).
injection hh; intros; auto.
simpls.
intros.
(**)
Focus 5.
case_var*; simpl.
case_nat*.
(**)
Focus 5.
rewrite H; auto.
intros; f_equal*.
assert (hh:= H0 x0).
injection hh; intros.
auto.
(**)
Focus 4.
rewrite H; auto.
rewrite H0; auto.
rewrite H1; auto.
intros.
assert (hh:=H2 x0).
injection hh; intros; auto.
intros.
assert (hh:=H2 x0).
injection hh; intros; auto.
intros.
assert (hh:=H2 x0).
injection hh; intros; auto.
(**)
Focus 3.
rewrite H; auto.
rewrite H0; auto.
intros.
assert (hh:=H1 x0).
injection hh; intros; auto.
intros.
assert (hh:=H1 x0).
injection hh; intros; auto.
(**)
Focus 2.
intros.
assert (hh:=H1 x0).
injection hh; intros; auto.
assert (hh:=H1 x0).
injection hh; intros; auto.
Qed.


Lemma open_close_var :
forall e y, y \notin fv e ->
close_var y (open e (fvar y)) = e.
Proof.
intros.
unfold close_var; unfold open.
generalize 0 y H; clear y H.
apply trmind with
(P:= fun e =>
forall n y, y \notin fv e ->
close_var_rec n y (open_rec n (fvar y) e) = e)
(P0:= fun e =>
forall n y, y \notin fv_exp e ->
close_var_exp n y (open_exp n (fvar y) e) = e)
(P1:= fun v =>
forall n y, y \notin fv_val v ->
close_var_val n y (open_val n (fvar y) v) = v)
(P2:= fun e =>
forall n y, y \notin fv_cont e ->
close_var_cont n y (open_cont n (fvar y) e) = e); simpl; intros; subst; 
try rewrite H; try rewrite H0; auto.
notin_simpl_hyps.
f_equal*.
case_nat*.
simpl.
case_var*.
case_var*.
(*notin_contradiction.*)
Qed.
(*
Lemma ttrm_subst_var :
forall e x v, ttrm e -> ttrm (subst e x (fvar v)).
Proof.
intros e.
apply trmind with
(P:= fun e => forall x v, ttrm e -> ttrm (subst e x (fvar v)))
(P0:=fun e => forall x v, texp e -> texp (subst_exp e x (fvar v)))
(P1:=fun v0' => forall x v, tval v0' -> tval (subst_val v0' x (fvar v)))
(P2:= fun c:cont => True)
(*ttrm e -> ttrm (c = let_cont e' ->
ttrm e' -> (*body e' -> *)
ttrm (subst_cont e' x (fvar v)))*); intros; simpl; auto.
constructor; auto.
apply H; auto.
inversions H0; auto.
(**)
inversions H1; simpl; constructor; auto.
(**)
inversions H1; simpl; constructor; auto.
(**)
inversions H1; simpl.
inversions H2; simpl.
constructor 3; auto.
(**)
case_var*; constructor.
(**)
inversions H0.
constructor; auto.
Qed.
*)
(*
Lemma open_ttrm :
forall u k y, ttrm (open_rec k (fvar y) u) ->
ttrm u.
Proof.
intros u.
apply trmind with
(P:=fun u => forall k y, ttrm (open_rec k (fvar y) u) -> ttrm u)
(P0:= fun e => forall k y, texp (open_exp k (fvar y) e) -> texp e)
(P1:=fun v => forall k y, tval (open_val k (fvar y) v) -> tval v)
(P2:= fun c:cont => True); simpl; intros; auto.
Focus 5.
case_nat*.
constructor.
(**)
Focus 5.
constructor.
(**)
Focus 4.
inversions H2.
induction c; simpls; try discriminate.
injection H6; intros; auto.
constructor; auto.
(**)
inversions H0.
constructor; auto.
apply H with (S k) y; auto.
(**)
inversions H1.
induction c; simpls; try discriminate.
injection H3; intros; subst.
constructor.
induction c; simpls; try discriminate.
constructor.
inversions H1.
Qed.
*)

Lemma open_open_exp :
forall e i k x y, i<>k -> 
open_exp i (fvar y) (open_exp k (fvar x) e)
= open_exp k (fvar x) (open_exp i (fvar y) e).
Proof.
intro e.
apply trmexpind with
(P := fun e =>
forall i k x y, i<>k -> 
open_rec i (fvar y) (open_rec k (fvar x) e)
= open_rec k (fvar x) (open_rec i (fvar y) e))
(P0 := fun e =>
forall i k x y, i<>k -> 
open_exp i (fvar y) (open_exp k (fvar x) e)
= open_exp k (fvar x) (open_exp i (fvar y) e))
(P1 := fun v =>
forall i k x y, i<>k -> 
open_val i (fvar y) (open_val k (fvar x) v)
= open_val k (fvar x) (open_val i (fvar y) v))
(P2 := fun c =>
forall i k x y, i<>k -> 
open_cont i (fvar y) (open_cont k (fvar x) c)
= open_cont k (fvar x) (open_cont i (fvar y) c));
intros; subst; simpl; auto.
rewrite H; auto.
(**)
rewrite H; auto.
rewrite H0; auto.
(**)
rewrite H; auto.
rewrite H0; auto.
(**)
rewrite H; auto.
rewrite H0; auto.
rewrite H1; auto.
(**)
rewrite H; auto.
rewrite H0; auto.
(**)
case_nat*; simpl.
case_nat*; simpl; auto.
case_nat*.
case_nat*.
simpl.
case_nat*.
(**)
rewrite H; auto.
(**)
rewrite H; auto.
Qed.


Lemma open_open :
forall e i k x y, i<>k -> 
open_rec i (fvar y) (open_rec k (fvar x) e)
= open_rec k (fvar x) (open_rec i (fvar y) e).
Proof.
intro e.
apply trmind with
(P := fun e =>
forall i k x y, i<>k -> 
open_rec i (fvar y) (open_rec k (fvar x) e)
= open_rec k (fvar x) (open_rec i (fvar y) e))
(P0 := fun e =>
forall i k x y, i<>k -> 
open_exp i (fvar y) (open_exp k (fvar x) e)
= open_exp k (fvar x) (open_exp i (fvar y) e))
(P1 := fun v =>
forall i k x y, i<>k -> 
open_val i (fvar y) (open_val k (fvar x) v)
= open_val k (fvar x) (open_val i (fvar y) v))
(P2 := fun c =>
forall i k x y, i<>k -> 
open_cont i (fvar y) (open_cont k (fvar x) c)
= open_cont k (fvar x) (open_cont i (fvar y) c));
intros; subst; simpl; auto.
rewrite H; auto.
(**)
rewrite H; auto.
rewrite H0; auto.
(**)
rewrite H; auto.
rewrite H0; auto.
(**)
rewrite H; auto.
rewrite H0; auto.
rewrite H1; auto.
(**)
rewrite H; auto.
rewrite H0; auto.
(**)
case_nat*; simpl.
case_nat*; simpl; auto.
case_nat*.
case_nat*.
simpl.
case_nat*.
(**)
rewrite H; auto.
(**)
rewrite H; auto.
Qed.


Lemma term_body :
forall e y, body e ->
term_cont (open_cont 0 (fvar y) (c_lam e)).
Proof.
unfold body; intros.
destruct H.
simpl.
constructor 2 with (x \u {{y}}); auto.
intros.
rewrite open_open_exp; auto.
rewrite term_open_exp; auto.
Qed.