(* 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.

Require Import cps_infrastructure_full.

Hint Extern 4 (term ?X) => constructor; auto.

Hint Extern 4 (term_val ?X) => constructor; auto.

Hint Extern 4 (?X ^ ?Y) => unfold open_rec.

Lemma closed_cps :
forall t, closed (cps t).
Proof.
induction t; simpl; repeat constructor; auto.
Qed.

Lemma term_cps :
forall t, term (cps t).
Proof.
induction t; simpl; auto.
constructor 1 with {}; simpl; intros; auto.
repeat constructor.
(**)
constructor 1 with {}; simpl; intros; auto.
repeat constructor.
rewrite term_openc;  auto.
(**)
constructor 1 with {}; simpl; intros; auto.
repeat constructor.
rewrite term_openc; auto.
constructor 2 with {}; intros; auto.
simpls.
repeat constructor; auto.
rewrite* term_open; rewrite* term_openc.
(**)
constructor 2 with {}; intros; simpls; auto.
repeat constructor.
(**)
constructor 1 with {}; intros; simpls; auto.
repeat constructor.
rewrite* term_openc.
constructor 2 with {}; intros; simpls; auto.
repeat constructor.
rewrite* term_openc.
rewrite* term_open.
Qed.


Lemma Rd_term_exp :
forall e0 e1, Rd e0 e1 -> term_exp e0 /\ term_exp e1.
Proof.
induction 1; simpls; auto.
Focus 2.
split; auto.
constructor.
constructor 2 with  L.
intros.
apply H; auto.
auto.
apply open_term_exp; auto.
unfold body.
split with L; apply H; auto.
(**)
split.
repeat constructor.
constructor 1 with L.
intros.
apply H; auto.
auto.
pick_fresh z.
notin_simpls.
assert (hh:=H z Fr).
replace (openc_exp 0 c e) with (substc_exp (openc_exp 0 (c_fid z) e) z c).
Focus 2.
rewrite substc_exp_openc; auto.
simpls.
case_var*.
rewrite substc_exp_fresh; auto.
apply substc_term_exp.
auto.
auto.
Qed.


Lemma Rd_backwards_preserves_Re :
forall e e', Rd e e' -> Re e' -> Re e.
Proof.
unfold Re; intros.
destruct H0.
split with x.
apply Ne_trans with e'; auto.
Qed.

(*
Lemma A_term_val :
forall v v', A v v' -> term_val v /\ term_val v'.
Proof.
intros v v'.
apply Aind with
(P:=fun v v' (H:A v v') => term_val v /\ term_val v')
(P0:=fun r0 r1 (H:N r0 r1) => term r0 /\ term r1)
(P1:=fun e0 r1 (H:Ne e0 r1) => term_exp e0 /\ term_exp r1) 
(P2:=fun c0 r1 (H:C c0 r1) => term_cont c0 /\ term_cont r1); intros; try destruct H; simpls; auto.
split; constructor 1 with L; intros; destruct (H k); auto.
split; repeat constructor; auto.
destruct H0; destruct H1; split; repeat constructor; auto.
split.
destruct (Rd_term_exp e0 e1); auto.
auto.
split; constructor.
split; constructor 2 with L; intros; destruct (H w); auto.
Qed.
*)

Lemma Ne_term_exp :
forall e0 e1, Ne e0 e1 -> term_exp e0 /\ term_exp e1.
Proof.
intros v v'.
apply Neind with
(P:=fun v v' (H:A v v') => term_val v /\ term_val v')
(P0:=fun r0 r1 (H:N r0 r1) => term r0 /\ term r1)
(P1:=fun e0 r1 (H:Ne e0 r1) => term_exp e0 /\ term_exp r1) 
(P2:=fun c0 r1 (H:C c0 r1) => term_cont c0 /\ term_cont r1); intros; try destruct H; simpls; auto.
split; constructor 1 with L; intros; destruct (H k); auto.
split; repeat constructor; auto.
destruct H0; destruct H1; split; repeat constructor; auto.
destruct H0; split; constructor; auto.
split.
destruct (Rd_term_exp e0 e1); auto.
auto.
split; try constructor.
split; constructor 2 with L; intros; destruct (H w); auto.
(*
constructor 2 with {}; intros; repeat constructor.
simpls.
constructor.
constructor.
constructor.
split; constructor 2 with L; intros; destruct (H w); auto.*)
Qed.

Lemma Ne_substc :
forall e0 e1, Ne e0 e1 ->
forall w, (*exists L,*) forall y, (*y \notin L ->*) Ne (substc_exp e0 w (c_fid y)) (substc_exp e1 w (c_fid y)).
Proof.
Proof.
intros e0 e1 H.
apply Neind with
(P:=fun v0 v1 (H:A v0 v1) =>
forall w y, A (substc_val v0 w (c_fid y)) (substc_val v1 w (c_fid y)))
(P1:=fun e0 e1 (H:Ne e0 e1) =>
forall w y, Ne (substc_exp e0 w (c_fid y)) (substc_exp e1 w (c_fid y)))
(P2:=fun c0 c1 (H:C c0 c1) =>
forall w y, C (substc_cont c0 w (c_fid y)) (substc_cont c1 w (c_fid y)))
(P0:=fun r0 r1 (H:N r0 r1) =>
forall w y, N (substc r0 w (c_fid y)) (substc r1 w (c_fid y)));
intros; simpls; auto.
constructor.
(**)
constructor.
apply H0; auto.
(**)
constructor 1 with (L \u {{w}}); intros.
replace (c_fid k) with (substc_cont (c_fid k) w (c_fid y)); auto.
rewrite <- substc_exp_openc.
rewrite <- substc_exp_openc.
apply H0; auto.
constructor.
constructor.
simpls.
case_var*.
(*notin_contradiction.*)
(**)
case_var*; simpls; repeat constructor; apply H0; auto.
(**)
constructor.
apply H0; auto.
apply H1; auto.
apply H2; auto.
(**)
constructor.
apply H0; auto.
auto.
(**)
constructor 4 with (substc_exp e3 w (c_fid y)); auto.
apply substc_rd; auto.
case_var*.
constructor.
constructor.
constructor 2 with (L \u {{w}}).
intros.
notin_simpls.
assert (hh:=H0 x Fr w y).
do 2 rewrite substc_exp_open in hh.
simpls.
auto.
constructor.
constructor.
constructor.
Qed.



Lemma Ne_subst :
forall e0 e1, Ne e0 e1 ->
forall w, (*exists L,*) forall y, (*y \notin L ->*) Ne (subst_exp e0 w (fvar y)) (subst_exp e1 w (fvar y)).
Proof.
intros e0 e1 H.
apply Neind with
(P:=fun v0 v1 (H:A v0 v1) =>
forall w y, (*exists L, forall y, y \notin L ->*) A (subst_val v0 w (fvar y)) (subst_val v1 w (fvar y)))
(P1:=fun e0 e1 (H:Ne e0 e1) =>
forall w y, (*exists L, forall y, y \notin L ->*) Ne (subst_exp e0 w (fvar y)) (subst_exp e1 w (fvar y)))
(P2:=fun c0 c1 (H:C c0 c1) =>
forall w y, (*exists L, forall y, y \notin L ->*) C (subst_cont c0 w (fvar y)) (subst_cont c1 w (fvar y)))
(P0:=fun r0 r1 (H:N r0 r1) =>
forall w y, (*exists L, forall y, y \notin L ->*) N (subst r0 w (fvar y)) (subst r1 w (fvar y)));
intros; simpls; auto.
case_var*; constructor.
(**)
constructor; auto.
(**)
constructor 1 with L; intros.
assert (hh:=H0 k H1 w y).
do 2 rewrite subst_exp_openc in hh.
simpls.
auto.
constructor.
constructor.
constructor.
(**)
repeat constructor.
apply H0; auto.
(**)
constructor.
apply H0; auto.
apply H1; auto.
apply H2; auto.
(**)
constructor.
apply H0; auto.
apply H1; auto.
(**)
constructor 4 with (subst_exp e3 w (fvar y)); auto.
apply subst_rd; auto.
constructor.
constructor 2 with (L \u {{w}}).
intros.
notin_simpls.
assert (hh:=H0 x Fr w y).
do 2 rewrite subst_exp_open in hh.
simpls.
case_var*.
constructor.
constructor.
constructor.
Qed.

Lemma term_eta_expand:
forall r x, closed r -> term r ->
forall k, k \notin fvc r -> 
Ne (trm_app r (c_fid k)) x -> N r (trm_term (closec_var_exp 0 k x)).
Proof.
induction r; intros.
inversions H0.
inversions H.
simpls.
inversions H2.
constructor 1 with L.
intros.
rewrite* closec_var_openc_exp.
Focus 2.
intros.
rewrite* term_openc_exp.
destruct (@Ne_term_exp e1 x); auto.
inversions H.
replace (openc_exp 0 (c_fid k0) e) with (substc_exp (openc_exp 0 (c_fid k) e) k (c_fid k0)).
apply Ne_substc; auto.
rewrite substc_exp_openc.
simpls.
case_var*.
rewrite* substc_exp_fresh.
constructor.
Qed.

Lemma cont_eta_expand:
forall e x, term_cont (c_lam e) ->
forall w, w \notin fv_cont (c_lam e) -> 
Ne (cont_app (c_lam e) (fvar w)) x -> C (c_lam e) (c_lam (close_var_exp 0 w x)).
Proof.
(*induction c; intros; try discriminate.
inversions H0.
inversions H.
inversions H5.
simpls.
case_var*.
constructor.
simpls.*)
intros.
inversions H1.
inversions H.
inversions H2.
constructor 2 with L; intros.
rewrite* close_var_open_exp.
Focus 2.
intros.
rewrite term_open_exp; auto.
destruct (@Ne_term_exp (open_exp 0 (fvar w) e) x); auto.
(*inversions H.*)
replace (open_exp 0 (fvar x0) e) with (subst_exp (open_exp 0 (fvar w) e) w (fvar x0)); auto.
apply Ne_subst; auto.
simpls.
rewrite subst_exp_open.
simpls.
case_var*.
rewrite subst_exp_fresh.
auto.
auto.
constructor.
Qed.

(*
Lemma cont_eta_expand:
forall c x, (*closed_cont c -> *) term_cont c ->
forall w, w \notin fv_cont c -> Ne (cont_app c (fvar w)) x -> C c (c_lam (close_var_exp 0 w x)).
Admitted.
*)
(*Proof.
induction c; intros; try discriminate.
inversions H.
inversions H1.
inversions H5.
simpls.
case_var*.
constructor.
simpls.
inversions H2.
inversions H1.
inversions H2.
constructor 2 with L; intros.
rewrite* close_var_open_exp.
Focus 2.
intros.
rewrite term_open_exp; auto.
destruct (@Ne_term_exp (cont_app (c_lam e) (fvar w)) x); auto.
inversions H2.
replace (open_exp 0 (fvar x0) e) with (subst_exp (open_exp 0 (fvar w) e) w (fvar x0)); auto.
apply Ne_subst; auto.
simpls.
rewrite subst_exp_open.
simpls.
case_var*.
rewrite subst_exp_fresh.
auto.
auto.
constructor.
Qed.
*)
(*unfold Re; intros.
destruct (H0 (fvar v)).
constructor.
constructor.
constructor.
split with (fvar v); auto.
constructor.
split with x; auto.
constructor 3 with (cont_app c (fvar v)); auto.
replace (cont_app c (fvar v)) with (openc_exp 0 c (cont_app (c_bid 0) (fvar v))); auto.
constructor 1 with {}; intros; auto.
simpl.
repeat constructor.
destruct (Ne_term_exp (cont_app c (fvar v)) x); auto.
inversions H1.
auto.
(**)
Focus 2.
assert (term_cont c).
pick_fresh z.
destruct (H0 (fvar z)).
repeat constructor.
split with (fvar z); constructor.
destruct (@Ne_term_exp _ x n).
inversions H1; auto.
unfolds R.
assert (Re (trm_app (cps t1) (c_lam (trm_app (cps t2) (c_lam (val_app (bvar 1)
(bvar 0) c)))))).
apply IHt1; auto.
unfold Gc.
split; repeat constructor.
apply closed_cps; auto.
destruct H; auto.
constructor 2 with {}.
intros.
simpls.
repeat constructor.
rewrite term_open; apply term_cps.
constructor 2 with {}; intros.
simpls.
repeat constructor.
rewrite term_cont_open; auto.
rewrite term_cont_open; auto.
rewrite term_cont_open; auto.  
unfold Rc.
intros.
assert (Re (trm_app (cps t2) (c_lam (val_app v (bvar 0) c)))).
apply IHt2; auto.
destruct H.
destruct H2.
destruct H3.
split; repeat constructor; auto.
constructor 2 with {}; intros.
simpls.
repeat constructor.
rewrite term_val_open; auto.
rewrite term_cont_open; auto.
unfold Rc; intros.
pick_fresh z.
notin_simpls.
assert (Re (cont_app c (fvar z))).
apply H0; auto.
constructor.
constructor.
constructor.
split with (fvar z); constructor.
destruct H4.
destruct H.
destruct H6.
assert (hh:=cont_eta_expand c x H H1 z Fr4 n).
destruct H3.
destruct H5.
split with (val_app x0 x1 (c_lam (close_var_exp 0 z x))).
constructor 3 with (val_app v v0 c); auto.
replace (val_app v v0 c) with (open_exp 0 v0 (val_app v (bvar 0) c)); auto.
constructor 2 with {}; auto.
intros.
simpls.
constructor; auto.
rewrite term_val_open.
destruct H2; auto.
destruct H2; auto.
rewrite term_cont_open; auto.
simpls.
destruct H2; auto.
simpls.
rewrite term_val_open; auto.
rewrite term_cont_open; auto.
constructor; auto.
unfold Re.
destruct H4.
split with x; auto.
constructor 3 with (trm_app (cps t2) (c_lam (val_app v (bvar 0) c))); auto.
replace (trm_app (cps t2) (c_lam (val_app v (bvar 0) c))) with
(open_exp 0 v (trm_app (cps t2) (c_lam (val_app (bvar 1) (bvar 0) c)))); auto.
constructor 2 with {}.
intros.
simpls.
constructor.
rewrite term_open; apply term_cps.
constructor 2 with {}; intros.
simpls.
repeat constructor.
rewrite term_cont_open; auto.
rewrite term_cont_open; auto.
rewrite term_cont_open; auto.
destruct H2; auto.
simpls.
rewrite term_open; try apply term_cps.
rewrite term_cont_open; auto.
destruct H2.
split with x.
constructor 3 with (trm_app (cps t1) (c_lam (trm_app (cps t2) (c_lam (val_app (bvar 1)
(bvar 0) c))))); auto.
replace (trm_app (cps t1) (c_lam (trm_app (cps t2) (c_lam (val_app (bvar 1)
(bvar 0) c))))) with
(openc_exp 0 c (trm_app (cps t1) (c_lam (trm_app (cps t2) (c_lam (val_app (bvar 1)
(bvar 0) (c_bid 2))))))); auto.
constructor 1 with {}; intros; auto.
simpls.
repeat constructor.
rewrite term_openc; apply term_cps; auto.
destruct H; repeat constructor.
constructor 2 with {}; intros; auto.
simpls.
repeat constructor.
rewrite term_openc.
rewrite term_open.
apply term_cps.
apply term_cps.
apply term_cps.
constructor 2 with {}; intros.
simpls.
repeat constructor.
simpls.
(*destruct H; auto.
simpls.*)
rewrite term_openc; auto.
rewrite term_openc; auto.
apply term_cps.
apply term_cps.
(**)
unfold Re.
assert (Re (cont_app c (lam v (cps t)))).
apply H0; auto.
split; auto.
constructor.
apply closed_cps.
constructor.
apply term_cps.
Focus 2.
destruct H1.
split with x; auto.
constructor 3 with (cont_app c (lam v (cps t))); auto.
replace (cont_app c (lam v (cps t))) with
(openc_exp 0 c (cont_app (c_bid 0) (lam v (cps t)))); auto.
constructor 1 with {}; intros.
simpls.
repeat constructor.
rewrite term_openc.
apply term_cps.
apply term_cps.
destruct (@Ne_term_exp _ x n); auto.
inversions H1; auto.
simpls.
rewrite term_openc; auto.
apply term_cps.
unfold R in IHt.
unfold Rv.
pick_fresh_for (fvc (cps t)) c0.
notin_simpls.
Print cont_eta_expand.
split with (cont_app (c_fid c0) x); constructor; auto.

(destruct (IHt (c_fid c0)).

unfolds Rc.
intros.
destruct H1.
split with (cont_app (c_fid c0) x); constructor; auto.
(*assert (c0 \notin fvc (cps t)).
intro.
Focus 2.*)
assert (hh:=term_eta_expand (cps t) x (closed_cps _) (term_cps _) c0 Fr n).
split with (lam v (trm_term (closec_var_exp 0 c0 x))); constructor; auto.
destruct H5.
*)

Scheme closedtermind := Induction for closed Sort Prop
with
closedvalind:=Induction for closed_val Sort Prop
with
closedexpind:=Induction for closed_exp Sort Prop
with
closedcontind:=Induction for closed_cont Sort Prop.


Lemma closed_fvc :
forall r, closed r -> forall x, x \notin fvc r.
Proof.
intros r H.
apply closedtermind with
(P:= fun r (H:closed r) => forall x, x \notin fvc r)
(P1:= fun r (H:closed_exp r) => forall x, x \notin fvc_exp r)
(P0:= fun r (H:closed_val r) => forall x, x \notin fvc_val r)
(P2:= fun r (H:closed_cont r) => forall x, x \notin fvc_cont r);
intros; try intro; notin_simpls; simpls; auto.
elim H0 with x; auto.
Focus 3.
elim H0 with x0; auto.
elim notin_empty with x0; auto.
elim notin_empty with x0; auto.
5: elim notin_empty with x; auto.
Focus 5.
assert (hh:=H0 x).
elim hh; auto.
assert (hh:=H0 x).
assert (hx:=H1 x).
destruct (notin_union x (fvc_cont c) (fvc_val v)).
apply H4; auto.
assert (hh:=H0 x).
assert (hx:=H1 x).
destruct (notin_union x (fvc r0) (fvc_cont c)).
apply H4; auto.
assert (hh:=H0 x).
assert (hx:=H1 x).
destruct (notin_union x (fvc_val v0 \u (fvc_val v1)) (fvc_cont c)).
apply H5; auto.
assert (hh:=H0 x0).
assert (hx:=H1 x0).
destruct (notin_union x0 (fvc_val v) (fvc_exp e)).
apply H4; auto.
Qed.

(*destruct (notin_union x (fvc_cont c) (fvc_val v)).
assert (hh:=H0 x).
assert (hx:=H1 x).
*)

Lemma aux :
forall k v, Gv v -> Rv v -> Re (cont_app (c_fid k) v).
Proof.
intros.
destruct H0.
split with (cont_app (c_fid k) x).
constructor.
auto.
Qed.

(*
Lemma aux2 :
forall c z, Rc c -> Re (cont_app c (fvar z)).
Proof.
intros.
generalize X; clear X; induction c; intros.
inversions X.
apply aux; try constructor.
constructor.
constructor.
split with (fvar z).
constructor.
apply X; auto.
repeat constructor.
split with (fvar z); constructor.
Qed.
*)

(*
Lemma main :
forall t, R (cps t).
Proof.
induction t; simpls; unfold R; intros; auto.
(* var *)
assert (Re (cont_app c (fvar v))).
generalize X; clear X; induction c; intros.
inversions X.
(* c_fid *)
split with (cont_app (c_fid k) (fvar v)).
constructor.
constructor.
(* c_lam *)
set (c:=c_lam e).
apply X; auto.
constructor.
constructor.
constructor.
split with (fvar v); constructor.
destruct H.
split with x; auto.
constructor 3 with (cont_app c (fvar v)); auto.
replace (cont_app c (fvar v)) with (openc_exp 0 c (cont_app (c_bid 0) (fvar v))); auto.
constructor 1 with {}; intros; auto.
simpl.
repeat constructor.
destruct (Ne_term_exp (cont_app c (fvar v)) x); auto.
inversions H.
auto.
(**)
Focus 2.
assert (term_cont c).
generalize X; clear X; induction c; intros.
inversions X.
constructor.
simpl in X.
pick_fresh z.
assert (Gv (fvar z)).
constructor.
constructor.
constructor.
assert (Rv (fvar z)).
split with (fvar z); constructor.
destruct (X _ H H0).
destruct (@Ne_term_exp _ _ n).
inversions H1.
auto.
assert (Re (trm_app (cps t1) (c_lam (trm_app (cps t2) (c_lam (val_app (bvar 1)
(bvar 0) c)))))).
apply IHt1; auto.
unfold Rc.
intros.
assert (Re (trm_app (cps t2) (c_lam (val_app v (bvar 0) c)))).
apply IHt2; auto.
unfold Rc; intros.
pick_fresh_for (fv_cont c) z.
notin_simpls.
assert (Re (cont_app c (fvar z))).


apply H; auto.
constructor.
constructor.
constructor.
split with (fvar z); constructor.
destruct H4.
destruct H5.
assert (hh:=cont_eta_expand c x0 H0 z Fr n).
destruct H2.
destruct H1.
split with (val_app x1 x (c_lam (close_var_exp 0 z x0))).
constructor 3 with (val_app v v0 c); auto.
replace (val_app v v0 c) with (open_exp 0 v0 (val_app v (bvar 0) c)); auto.
constructor 2 with {}; auto.
intros.
simpls.
constructor; auto.
rewrite term_val_open.
destruct H0; auto.
destruct H0; auto.
rewrite term_cont_open; auto.
destruct H3; auto.
simpls.
rewrite term_val_open; auto.
rewrite term_cont_open; auto.
constructor; auto.
unfold Re.
destruct H3.
split with x; auto.
constructor 3 with (trm_app (cps t2) (c_lam (val_app v (bvar 0) c))); auto.
replace (trm_app (cps t2) (c_lam (val_app v (bvar 0) c))) with
(open_exp 0 v (trm_app (cps t2) (c_lam (val_app (bvar 1) (bvar 0) c)))); auto.
constructor 2 with {}.
intros.
simpls.
constructor.
rewrite term_open; apply term_cps.
constructor 2 with {}; intros.
simpls.
repeat constructor.
rewrite term_cont_open; auto.
rewrite term_cont_open; auto.
rewrite term_cont_open; auto.
destruct H1; auto.
simpls.
rewrite term_open; try apply term_cps.
rewrite term_cont_open; auto.
destruct H1.
split with x.
constructor 3 with (trm_app (cps t1) (c_lam (trm_app (cps t2) (c_lam (val_app (bvar 1)
(bvar 0) c))))); auto.
replace (trm_app (cps t1) (c_lam (trm_app (cps t2) (c_lam (val_app (bvar 1)
(bvar 0) c))))) with
(openc_exp 0 c (trm_app (cps t1) (c_lam (trm_app (cps t2) (c_lam (val_app (bvar 1)
(bvar 0) (c_bid 2))))))); auto.
constructor 1 with {}; intros; auto.
simpls.
repeat constructor.
rewrite term_openc; apply term_cps; auto.
(*unfold Gc in H.
destruct H; repeat constructor.
constructor 2 with {}; intros; auto.
simpls.
repeat constructor.
rewrite term_openc.
rewrite term_open.
apply term_cps.
apply term_cps.
apply term_cps.*)
constructor 2 with {}; intros.
simpls.
repeat constructor.
(*destruct H; auto.
simpls.*)
rewrite term_openc; auto.
rewrite term_open; auto.
apply term_cps.
apply term_cps.
apply term_cps.
(*Focus 2.
destruct (@Ne_term_exp _ x n).
inversions H0.
inversions H5.
pick_fresh z.
notin_simpls.
assert (hh:=H3 z Fr).
inversions hh.
inversions H8.
pick_fresh z'.
notin_simpls.
assert (hx:=H6 z' Fr10).
inversions hx.
inversions H14.
apply IHt1.*)
constructor 2 with {}; intros.
simpls.
repeat constructor.
simpls.
rewrite term_openc; try apply term_cps.
rewrite term_openc; try apply term_cps.
auto.
(* case lam *)
unfold Re.
assert (Re (cont_app c (lam v (cps t)))).
apply H; auto.
split; auto.
constructor.
apply closed_cps.
constructor.
apply term_cps.
Focus 2.
destruct H0.
split with x; auto.
constructor 3 with (cont_app c (lam v (cps t))); auto.
replace (cont_app c (lam v (cps t))) with
(openc_exp 0 c (cont_app (c_bid 0) (lam v (cps t)))); auto.
constructor 1 with {}; intros.
simpls.
repeat constructor.
rewrite term_openc.
apply term_cps.
apply term_cps.
destruct (@Ne_term_exp _ x n); auto.
inversions H0; auto.
simpls.
rewrite term_openc; auto.
apply term_cps.
unfold R in IHt.
unfold Rv.
induction c.
assert (Gv (fvar v)).
constructor.
constructor.
constructor.
assert (Rv (fvar v)).
split with (fvar v); constructor.
assert (hh:=H (fvar v) H0 H1).
destruct hh.
assert False.
inversions n0.
inversions H2.
contradiction.
(* continuation variable *)
destruct (IHt (c_fid k)).
unfolds Rc.
intros.
destruct H1.
split with (cont_app (c_fid k) x); constructor; auto.
assert (hh:=term_eta_expand (cps t) x (closed_cps _) (term_cps _) k).
assert (k\notin fvc (cps t)).
apply closed_fvc.
apply closed_cps.
split with (lam v (trm_term (closec_var_exp 0 k x))); constructor; auto.
(* continuation function *)
pick_fresh_for {} c0.
notin_simpls.
destruct (IHt (c_fid c0)).
unfolds Rc.
intros.
destruct H1.
split with (cont_app (c_fid c0) x); constructor; auto.
assert (hh:=term_eta_expand (cps t) x (closed_cps _) (term_cps _) c0).
assert (c0\notin fvc (cps t)).
apply closed_fvc.
apply closed_cps.
split with (lam v (trm_term (closec_var_exp 0 c0 x))); constructor; auto.
Qed.
*)


Lemma main :
forall t, R (cps t).
Proof.
induction t; simpls; unfold R; unfold Rc; intros; auto.
destruct (H (fvar v)).
constructor.
constructor.
constructor.
split with (fvar v); auto.
constructor.
induction c.
(* c_bid *)
assert False.
inversions n.
inversions H0.
contradiction.
(* c_fid *)
split with (cont_app (c_fid k) (fvar v)).
constructor 4 with (openc_exp 0 (c_fid k) (cont_app (c_bid 0) (fvar v))).
constructor 1 with {}; auto.
intros.
simpls.
repeat constructor.
constructor.
simpls.
constructor.
constructor.
(* c_lam *)
set (c:=c_lam e).
split with x; auto.
constructor 4 with (cont_app c (fvar v)); auto.
replace (cont_app c (fvar v)) with (openc_exp 0 c (cont_app (c_bid 0) (fvar v))); auto.
constructor 1 with {}; intros; auto.
simpl.
repeat constructor.
destruct (Ne_term_exp (cont_app c (fvar v)) x); auto.
inversions H0.
auto.
(**)
Focus 2.
assert (term_cont c).
pick_fresh z.
destruct (H (fvar z)).
repeat constructor.
split with (fvar z); constructor.
destruct (@Ne_term_exp _ x n).
inversions H0; auto.
unfolds R.
assert (Re (trm_app (cps t1) (c_lam (trm_app (cps t2) (c_lam (val_app (bvar 1)
(bvar 0) c)))))).
apply IHt1; auto.
unfold Rc.
intros.
assert (Re (trm_app (cps t2) (c_lam (val_app v (bvar 0) c)))).
apply IHt2; auto.
unfold Rc; intros.
pick_fresh_for (fv_cont c) z.
notin_simpls.
assert (Re (cont_app c (fvar z))).
apply H; auto.
constructor.
constructor.
constructor.
split with (fvar z); constructor.
destruct H4.
destruct H5.
assert ({w:cont | C c w}).
induction c.
assert False.
inversions H0.
contradiction.
split with (c_fid k); constructor.
assert (hh:=cont_eta_expand e x0 H0 z Fr n).
split with (c_lam (close_var_exp 0 z x0)).
auto.
destruct H4.
destruct H2.
split with (val_app x2 x x1).
(*(c_lam (close_var_exp 0 z x0))).*)
constructor 4 with (val_app v v0 c); auto.
replace (val_app v v0 c) with (open_exp 0 v0 (val_app v (bvar 0) c)); auto.
constructor 2 with {}; auto.
intros.
simpls.
constructor; auto.
rewrite term_val_open.
destruct H0; auto.
destruct H1; auto.
destruct H1; auto.
destruct H1; auto.
rewrite term_cont_open; auto.
destruct H3; auto.
simpls.
rewrite term_val_open; auto.
rewrite term_cont_open; auto.
destruct H1; auto.
constructor; auto.
unfold Re.
destruct H3.
split with x; auto.
constructor 4 with (trm_app (cps t2) (c_lam (val_app v (bvar 0) c))); auto.
replace (trm_app (cps t2) (c_lam (val_app v (bvar 0) c))) with
(open_exp 0 v (trm_app (cps t2) (c_lam (val_app (bvar 1) (bvar 0) c)))); auto.
constructor 2 with {}.
intros.
simpls.
constructor.
rewrite term_open; apply term_cps.
constructor 2 with {}; intros.
simpls.
repeat constructor.
rewrite term_cont_open; auto.
rewrite term_cont_open; auto.
rewrite term_cont_open; auto.
destruct H1; auto.
simpls.
rewrite term_open; try apply term_cps.
rewrite term_cont_open; auto.
destruct H1.
split with x.
constructor 4 with (trm_app (cps t1) (c_lam (trm_app (cps t2) (c_lam (val_app (bvar 1)
(bvar 0) c))))); auto.
replace (trm_app (cps t1) (c_lam (trm_app (cps t2) (c_lam (val_app (bvar 1)
(bvar 0) c))))) with
(openc_exp 0 c (trm_app (cps t1) (c_lam (trm_app (cps t2) (c_lam (val_app (bvar 1)
(bvar 0) (c_bid 2))))))); auto.
constructor 1 with {}; intros; auto.
simpls.
repeat constructor.
rewrite term_openc; apply term_cps; auto.
(*unfold Gc in H.
destruct H; repeat constructor.
constructor 2 with {}; intros; auto.
simpls.
repeat constructor.
rewrite term_openc.
rewrite term_open.
apply term_cps.
apply term_cps.
apply term_cps.*)
constructor 2 with {}; intros.
simpls.
repeat constructor.
(*destruct H; auto.
simpls.*)
rewrite term_openc; auto.
rewrite term_open; auto.
apply term_cps.
apply term_cps.
apply term_cps.
(*Focus 2.
destruct (@Ne_term_exp _ x n).
inversions H0.
inversions H5.
pick_fresh z.
notin_simpls.
assert (hh:=H3 z Fr).
inversions hh.
inversions H8.
pick_fresh z'.
notin_simpls.
assert (hx:=H6 z' Fr10).
inversions hx.
inversions H14.
apply IHt1.*)
constructor 2 with {}; intros.
simpls.
repeat constructor.
simpls.
rewrite term_openc; try apply term_cps.
rewrite term_openc; try apply term_cps.
auto.
(* case lam *)
unfold Re.
induction c.
(* c_bid *)
assert False.
pick_fresh z.
notin_simpls.
destruct (H (fvar z)).
constructor.
constructor.
constructor.
split with (fvar z).
constructor.
inversions n0.
inversions H1.
contradiction.
(* c_fid *)
(*assert (Re (cont_app c (lam v (cps t)))).
apply H; auto.
split; auto.
constructor.
apply closed_cps.
constructor.
apply term_cps.*)
assert (Rc (c_fid k)).
unfold Rc.
intros.
destruct H1.
split with (cont_app (c_fid k) x).
constructor.
auto.
assert (Rv (lam v (cps t))).
pick_fresh j.
notin_simpls.
assert (Rc (c_fid j)).
unfold Rc.
intros.
destruct H4.
split with (cont_app (c_fid j) x).
constructor.
auto.
assert (hh:=IHt (c_fid j) H3).
destruct hh.
assert (N (cps t) (trm_term (closec_var_exp 0 j x))).
apply term_eta_expand; auto.
apply closed_cps.
apply term_cps.
apply closed_fvc.
apply closed_cps.
split with (lam v (trm_term (closec_var_exp 0 j x))).
repeat constructor.
auto.
destruct H1.
split with (cont_app (c_fid k) x).
constructor 4 with (openc_exp 0 (c_fid k) (cont_app (c_bid 0) (lam v (cps t)))).
constructor 1 with {}; auto.
intros.
simpls.
repeat constructor.
rewrite term_openc.
apply term_cps.
apply term_cps.
constructor.
simpls.
constructor.
rewrite term_openc.
auto.
apply term_cps.
(* c_lam *) 
set (c:=c_lam e).
assert (Re (cont_app c (lam v (cps t)))).
apply H; auto.
split; auto.
constructor.
apply closed_cps.
constructor.
apply term_cps.
pick_fresh k.
assert (Rc (c_fid k)).
unfold Rc.
intros.
destruct H1.
split with (cont_app (c_fid k) x).
constructor.
auto.
assert (hh:=IHt (c_fid k) H0).
destruct hh.
assert (N (cps t) (trm_term (closec_var_exp 0 k x))).
apply term_eta_expand; auto.
apply closed_cps.
apply term_cps.
apply closed_fvc.
apply closed_cps.
split with (lam v (trm_term (closec_var_exp 0 k x))).
repeat constructor.
auto.
(*
induction c.
inversions H0.
assert False.
inversions H1.
inversions H2.
contradiction.
unfold R in IHt.
assert (hh:=IHt (c_fid k) (aux k)).
destruct hh.
assert (hh:=term_eta_expand (cps t) x (closed_cps _) (term_cps _) k).
split with (cont_app (c_fid k) (lam v (trm_term (closec_var_exp 0 k x)))).
constructor 3 with (openc_exp 0 (c_fid k) (cont_app (c_bid 0) (lam v (cps t)))).
constructor 1 with {}; auto.
intros.
simpls.
repeat constructor.
rewrite term_openc.
apply term_cps.
apply term_cps.
constructor.
simpls.
repeat constructor.
rewrite term_openc; auto.
apply hh; auto.
apply closed_fvc.
apply closed_cps.
apply term_cps.
*)
destruct H0.
(*set (c:=c_lam e).*)
split with x; auto.
constructor 4 with (cont_app c (lam v (cps t))); auto.
replace (cont_app c (lam v (cps t))) with
(openc_exp 0 c (cont_app (c_bid 0) (lam v (cps t)))); auto.
constructor 1 with {}; intros.
simpls.
repeat constructor.
rewrite term_openc.
apply term_cps.
apply term_cps.
destruct (@Ne_term_exp _ x n); auto.
inversions H0; auto.
simpls.
rewrite term_openc; auto.
apply term_cps.
(* case let *)
unfold Re.
assert (Re 
(trm_app (cps t1) (c_lam (elet v (bvar 0) (trm_app (cps t2) c))))).
unfold R in IHt1.
apply IHt1; auto.
Focus 2.
destruct H0.
split with x; auto.
constructor 4 with
(openc_exp 0 c (trm_app (cps t1) (c_lam (elet v (bvar 0) (trm_app (cps t2) (c_bid 1)))))).
constructor 1 with {}; auto.
intros.
simpls.
rewrite term_openc.
rewrite term_openc.
repeat constructor.
apply term_cps.
constructor 2 with {}; intros; auto.
simpls.
repeat constructor.
rewrite term_open.
apply term_cps.
apply term_cps.
apply term_cps.
apply term_cps.
pick_fresh z.
destruct (H (fvar z)).
repeat constructor.
split with (fvar z); constructor.
destruct (@Ne_term_exp _ x0 n0).
inversions H0; auto.
simpls.
rewrite term_openc.
rewrite term_openc.
auto.
apply term_cps.
apply term_cps.
unfold Rc; intros.
destruct H0; destruct H1.
assert (Re (elet v v0 (trm_app (cps t2) c))).
unfold R in IHt2.
unfold Re.
assert (hh:=IHt2 c H).
destruct hh.
split with (elet v x x0).
constructor; auto.
destruct H1.
split with x0; auto.
constructor 4 with
(open_exp 0 v0 (elet v (bvar 0) (trm_app (cps t2) c))).
constructor 2 with {}; auto.
intros.
simpls.
rewrite term_open.
rewrite term_cont_open.
repeat constructor.
apply term_cps.
3: apply term_cps.
Focus 3.
simpls.
rewrite term_open; auto.
rewrite term_cont_open; auto.
2: apply term_cps.
pick_fresh z.
destruct (H (fvar z)).
repeat constructor.
split with (fvar z); constructor.
destruct (@Ne_term_exp _ x1 n0).
inversions H1; auto.
pick_fresh z.
destruct (H (fvar z)).
repeat constructor.
split with (fvar z); constructor.
destruct (@Ne_term_exp _ x2 n0).
inversions H3; auto.
pick_fresh z.
destruct (H (fvar z)).
repeat constructor.
split with (fvar z); constructor.
destruct (@Ne_term_exp _ x2 n0).
inversions H3; auto.
Qed.

(*


Lemma main :
forall t, R (cps t).
Proof.
induction t; simpls; unfold R; intros; auto.
Focus 3.
assert (term_cont c).
induction c; simpls.
contradiction.
constructor.
pick_fresh w.
notin_simpls.
assert (Gv (fvar w)).
constructor.
constructor.
constructor.
assert (Rv (fvar w)).
split with (fvar w); constructor.
assert (hx:=X (fvar w) H H0).
destruct hx. 
destruct (@Ne_term_exp _ _ n).
inversions H1.
auto.
(*pick_fresh z.
destruct (X (fvar z)).
repeat constructor.
split with (fvar z); constructor.
destruct (@Ne_term_exp _ x n).
inversions H0; auto.
unfolds R.*)
assert (Re (trm_app (cps t1) (c_lam (trm_app (cps t2) (c_lam (val_app (bvar 1)
(bvar 0) c)))))).
apply IHt1; auto.
unfold Rc.
intros.
assert (Re (trm_app (cps t2) (c_lam (val_app v (bvar 0) c)))).
apply IHt2; auto.
unfold Rc; intros.
pick_fresh_for (fv_cont c) z.
notin_simpls.
assert (Re (cont_app c (fvar z))).
generalize X; clear X; induction c; simpls; intros; auto.
contradiction.
split with (cont_app (c_fid k) (fvar z)).
constructor.
constructor.
apply X; auto.
constructor.
constructor.
constructor.
split with (fvar z).
constructor.
destruct H1.
destruct H3.
destruct H4.
(*assert (term_cont c).
destruct (@Ne_term_exp _ _ n).
inversions H0.
auto.*)
assert (hh:=@cont_eta_expand c x1 H z Fr n).
split with (val_app x x0 (c_lam (close_var_exp 0 z x1))).
constructor 3 with (open_exp 0 v0 (val_app v  (bvar 0) c)).
constructor 2 with {}; auto.
intros.
simpls.
constructor; auto.
rewrite term_val_open.
destruct H0; auto.
destruct H0; auto.
rewrite term_cont_open.
auto.
auto.
destruct H2; auto.
simpls.
constructor; auto.
rewrite term_val_open; auto.
destruct H0; auto.
rewrite term_cont_open; auto.
unfold Re.
destruct H2.
split with x; auto.
constructor 3 with (trm_app (cps t2) (c_lam (val_app v (bvar 0) c))); auto.
replace (trm_app (cps t2) (c_lam (val_app v (bvar 0) c))) with
(open_exp 0 v (trm_app (cps t2) (c_lam (val_app (bvar 1) (bvar 0) c)))); auto.
constructor 2 with {}.
intros.
simpls.
constructor.
rewrite term_open; apply term_cps.
constructor 2 with {}; intros.
simpls.
repeat constructor.
rewrite term_cont_open; auto.
rewrite term_cont_open; auto.
rewrite term_cont_open; auto.
destruct H0; auto.
simpls.
rewrite term_open; try apply term_cps.
rewrite term_cont_open; auto.
destruct H0.
split with x.
constructor 3 with (trm_app (cps t1) (c_lam (trm_app (cps t2) (c_lam (val_app (bvar 1)
(bvar 0) c))))); auto.
replace (trm_app (cps t1) (c_lam (trm_app (cps t2) (c_lam (val_app (bvar 1)
(bvar 0) c))))) with
(openc_exp 0 c (trm_app (cps t1) (c_lam (trm_app (cps t2) (c_lam (val_app (bvar 1)
(bvar 0) (c_bid 2))))))); auto.
constructor 1 with {}; intros; auto.
simpls.
repeat constructor.
rewrite term_openc; apply term_cps; auto.
constructor 2 with {}; intros.
simpls.
repeat constructor.
(*destruct H; auto.
simpls.*)
rewrite term_openc; auto.
rewrite term_open; auto.
apply term_cps.
apply term_cps.
apply term_cps.
constructor 2 with {}; intros.
simpls.
repeat constructor.
simpls.
rewrite term_openc; try apply term_cps.
rewrite term_openc; try apply term_cps.
auto.
(* var *)
generalize X; clear X; induction c; intros.
contradiction.
unfold Re.
split with (cont_app (c_fid k) (fvar v)).
constructor 3 with (openc_exp 0 (c_fid k) (cont_app (c_bid 0) (fvar v))).
constructor 1 with {}; intros; auto.
simpls.
repeat constructor.
constructor.
simpls.
constructor.
constructor.
(* var 2 *)
destruct (X (fvar v)).
constructor.
constructor.
constructor.
split with (fvar v); auto.
constructor.
split with x; auto.
constructor 3 with (cont_app (c_lam e) (fvar v)); auto.
replace (cont_app (c_lam e) (fvar v)) with (openc_exp 0 (c_lam e) (cont_app (c_bid 0) (fvar v))); auto.
constructor 1 with {}; intros; auto.
simpl.
repeat constructor.
constructor 2 with {}.
intros.
apply open_term_exp.
destruct (Ne_term_exp (cont_app (c_lam e) (fvar v)) x); auto.
inversions H0.
inversions H4.
unfold body.
split with L; auto.
constructor.
(* end of var *)
(*unfold Re.
generalize X; clear X; induction c; intros.
inversions X.
set (c:=c_fid k).
assert (Re (cont_app c (lam v (cps t)))).
apply IHt; auto.
split; auto.
constructor.
apply closed_cps.
constructor.
apply term_cps.
Focus 2.
destruct H0.
(*generalize X; clear X; induction c; intros.
inversions X.
destruct X.*)
split with x; auto.
constructor 3 with (cont_app c (lam v (cps t))); auto.
replace (cont_app c (lam v (cps t))) with
(openc_exp 0 c (cont_app (c_bid 0) (lam v (cps t)))); auto.
constructor 1 with {}; intros.
simpls.
repeat constructor.
rewrite term_openc.
apply term_cps.
apply term_cps.
destruct (@Ne_term_exp _ x n); auto.
inversions H0; auto.
simpls.
rewrite term_openc; auto.
apply term_cps.
unfold R in IHt.
unfold Rv.
induction c.
assert (Gv (fvar v)).
constructor.
constructor.
constructor.
assert (Rv (fvar v)).
split with (fvar v); constructor.
assert (hh:=H (fvar v) H0 H1).
destruct hh.
assert False.
inversions n0.
inversions H2.
contradiction.
(* continuation variable *)
destruct (IHt (c_fid k)).
unfolds Rc.
intros.
destruct H1.
split with (cont_app (c_fid k) x); constructor; auto.
assert (hh:=term_eta_expand (cps t) x (closed_cps _) (term_cps _) k).
assert (k\notin fvc (cps t)).
apply closed_fvc.
apply closed_cps.
split with (lam v (trm_term (closec_var_exp 0 k x))); constructor; auto.
(* continuation function *)
pick_fresh_for {} c0.
notin_simpls.
destruct (IHt (c_fid c0)).
unfolds Rc.
intros.
destruct H1.
split with (cont_app (c_fid c0) x); constructor; auto.
assert (hh:=term_eta_expand (cps t) x (closed_cps _) (term_cps _) c0).
assert (c0\notin fvc (cps t)).
apply closed_fvc.
apply closed_cps.
split with (lam v (trm_term (closec_var_exp 0 c0 x))); constructor; auto.


generalize X; clear X; induction c; intros.
inversions X.

set (c:=c_fid k).
assert (term_cont c).
subst c.
constructor.
(*pick_fresh z.
destruct (X (fvar z)).
repeat constructor.
split with (fvar z); constructor.
destruct (@Ne_term_exp _ x n).
inversions H0; auto.
unfolds R.*)
assert (Re (trm_app (cps t1) (c_lam (trm_app (cps t2) (c_lam (val_app (bvar 1)
(bvar 0) c)))))).
apply IHt1; auto.
unfold Rc.
intros.
assert (Re (trm_app (cps t2) (c_lam (val_app v (bvar 0) c)))).
apply IHt2; auto.
unfold Rc; intros.
pick_fresh_for (fv_cont c) z.
notin_simpls.
assert (Re (cont_app c (fvar z))).
subst c.
split with (cont_app (c_fid k) (fvar z)).
constructor.
constructor.
destruct H1.
destruct H3.
split with (val_app x x0 c).
constructor 3 with (open_exp 0 v0 (val_app v  (bvar 0) c)).
constructor 2 with {}; auto.
intros.
simpls.
constructor; auto.
rewrite term_val_open.
destruct H0; auto.
destruct H0; auto.
destruct H2; auto.
simpls.
constructor; auto.
rewrite term_val_open; auto.
destruct H0; auto.
subst c.
constructor.
unfold Re.
destruct H2.
split with x; auto.
constructor 3 with (trm_app (cps t2) (c_lam (val_app v (bvar 0) c))); auto.
replace (trm_app (cps t2) (c_lam (val_app v (bvar 0) c))) with
(open_exp 0 v (trm_app (cps t2) (c_lam (val_app (bvar 1) (bvar 0) c)))); auto.
constructor 2 with {}.
intros.
simpls.
constructor.
rewrite term_open; apply term_cps.
constructor 2 with {}; intros.
simpls.
repeat constructor.
destruct H1; auto.
destruct H0; auto.
simpls.
rewrite term_open; try apply term_cps.
subst c; auto.
destruct H0.
split with x.
constructor 3 with (trm_app (cps t1) (c_lam (trm_app (cps t2) (c_lam (val_app (bvar 1)
(bvar 0) c))))); auto.
replace (trm_app (cps t1) (c_lam (trm_app (cps t2) (c_lam (val_app (bvar 1)
(bvar 0) c))))) with
(openc_exp 0 c (trm_app (cps t1) (c_lam (trm_app (cps t2) (c_lam (val_app (bvar 1)
(bvar 0) (c_bid 2))))))); auto.
constructor 1 with {}; intros; auto.
simpls.
repeat constructor.
rewrite term_openc; apply term_cps; auto.
constructor 2 with {}; intros.
simpls.
repeat constructor.
(*destruct H; auto.
simpls.*)
rewrite term_openc; auto.
rewrite term_open; auto.
apply term_cps.
apply term_cps.
apply term_cps.
constructor 2 with {}; intros.
simpls.
repeat constructor.
simpls.
rewrite term_openc; try apply term_cps.
rewrite term_openc; try apply term_cps.
auto.

set (c:=c_lam e).
assert (term_cont c).
pick_fresh z.
simpl in X.
destruct (X (fvar z)).
repeat constructor.
split with (fvar z); constructor.
destruct (@Ne_term_exp _ x n).
inversions H0; auto.
unfolds R.
assert (Re (trm_app (cps t1) (c_lam (trm_app (cps t2) (c_lam (val_app (bvar 1)
(bvar 0) c)))))).
apply IHt1; auto.
unfold Rc.
intros.
assert (Re (trm_app (cps t2) (c_lam (val_app v (bvar 0) c)))).
apply IHt2; auto.
unfold Rc; intros.
destruct H4.
destruct H6.
assert (hh:=cont_eta_expand c e H1 z Fr n).
destruct H2.
destruct H1.
split with (val_app x x (c_lam (close_var_exp 0 z x0))).
constructor 3 with (val_app v v0 c); auto.
replace (val_app v v0 c) with (open_exp 0 v0 (val_app v (bvar 0) c)); auto.
constructor 2 with {}; auto.
intros.
simpls.
constructor; auto.
rewrite term_val_open.
destruct H0; auto.
destruct H0; auto.
rewrite term_cont_open; auto.
destruct H3; auto.
simpls.
rewrite term_val_open; auto.
rewrite term_cont_open; auto.
constructor; auto.
unfold Re.
destruct H3.
split with x; auto.
constructor 3 with (trm_app (cps t2) (c_lam (val_app v (bvar 0) c))); auto.
replace (trm_app (cps t2) (c_lam (val_app v (bvar 0) c))) with
(open_exp 0 v (trm_app (cps t2) (c_lam (val_app (bvar 1) (bvar 0) c)))); auto.
constructor 2 with {}.
intros.
simpls.
constructor.
rewrite term_open; apply term_cps.
constructor 2 with {}; intros.
simpls.
repeat constructor.
rewrite term_cont_open; auto.
rewrite term_cont_open; auto.
rewrite term_cont_open; auto.
destruct H1; auto.
simpls.
rewrite term_open; try apply term_cps.
rewrite term_cont_open; auto.
destruct H1.
split with x.
constructor 3 with (trm_app (cps t1) (c_lam (trm_app (cps t2) (c_lam (val_app (bvar 1)
(bvar 0) c))))); auto.
replace (trm_app (cps t1) (c_lam (trm_app (cps t2) (c_lam (val_app (bvar 1)
(bvar 0) c))))) with
(openc_exp 0 c (trm_app (cps t1) (c_lam (trm_app (cps t2) (c_lam (val_app (bvar 1)
(bvar 0) (c_bid 2))))))); auto.
constructor 1 with {}; intros; auto.
simpls.
repeat constructor.
rewrite term_openc; apply term_cps; auto.
constructor 2 with {}; intros.
simpls.
repeat constructor.
rewrite term_openc; auto.
rewrite term_open; auto.
apply term_cps.
apply term_cps.
apply term_cps.
constructor 2 with {}; intros.
simpls.
repeat constructor.
simpls.
rewrite term_openc; try apply term_cps.
rewrite term_openc; try apply term_cps.
auto.*)
(* case lam *)
unfold Re.
assert (Re (cont_app c (lam v (cps t)))).
(*apply H; auto.
split; auto.
constructor.
apply closed_cps.
constructor.
apply term_cps.*)
Focus 2.
destruct H.
split with x; auto.
constructor 3 with (cont_app c (lam v (cps t))); auto.
replace (cont_app c (lam v (cps t))) with
(openc_exp 0 c (cont_app (c_bid 0) (lam v (cps t)))); auto.
constructor 1 with {}; intros.
simpls.
repeat constructor.
rewrite term_openc.
apply term_cps.
apply term_cps.
destruct (@Ne_term_exp _ x n); auto.
inversions H; auto.
simpls.
rewrite term_openc; auto.
apply term_cps.
unfold R in IHt.
generalize X; clear X; induction c; intros.
inversions X.
(*assert (Gv (fvar v)).
constructor.
constructor.
constructor.
assert (Rv (fvar v)).
split with (fvar v); constructor.
assert (hh:=H (fvar v) H0 H1).
destruct hh.
assert False.
inversions n0.
inversions H2.
contradiction.*)
(* continuation variable *)
destruct (IHt (c_fid k)).
auto.
(*split with (cont_app (c_fid k) x); constructor; auto.*)
assert (hh:=term_eta_expand (cps t) x (closed_cps _) (term_cps _) k).
assert (k\notin fvc (cps t)).
apply closed_fvc.
apply closed_cps.
assert (hx:=hh H n).
split with (cont_app (c_fid k) (lam v (trm_term (closec_var_exp 0 k x)))); constructor; auto.
constructor.
auto.
(* continuation function *)
pick_fresh_for {} c0.
notin_simpls.
destruct (IHt (c_fid c0)).
simpls.
auto.
(*destruct H1.*)
(*split with (cont_app (c_fid c0) x); constructor; auto.*)
assert (hh:=term_eta_expand (cps t) x (closed_cps _) (term_cps _) c0).
assert (c0\notin fvc (cps t)).
apply closed_fvc.
apply closed_cps.
assert (hx:=hh H n).
unfold Rc in X.
apply X; auto.
constructor.
constructor.
apply closed_cps.
constructor.
apply term_cps.
split with (lam v (trm_term (closec_var_exp 0 c0 x))).
constructor.
auto.
Qed.

*)