Require Import List.
Require Import Program.
Require Import FunctionalExtensionality.
Require Import Omega.
Require Import Heq.
Require Import sysf.

Set Implicit Arguments.
Unset Strict Implicit.

Definition proj2m (A B C : Prop) (p: A /\ B /\ C) : B := proj1(proj2 p).
Definition proj3 (A B C : Prop) (p: A /\ B /\ C) : C := proj2(proj2 p).
Definition proj3m (A B C D : Prop) (p: A /\ B /\ C /\ D) : C := proj1(proj2(proj2 p)).
Definition proj4 (A B C D : Prop) (p: A /\ B /\ C /\ D) : D := proj2(proj2(proj2 p)).
Definition proj4m (A B C D E : Prop) (p: A /\ B /\ C /\ D /\ E) : D := proj1(proj2(proj2(proj2 p))).
Definition proj5 (A B C D E : Prop) (p: A /\ B /\ C /\ D /\ E) : E := proj2(proj2(proj2(proj2 p))).

Require Import Ensembles.
Lemma iff_implies_eq: forall (P Q:Prop), (P <-> Q) -> P = Q.
intros.
set (prop_ens := fun (P:Prop) => fun (_:unit) => P).
assert (prop_ens P = prop_ens Q).
apply Extensionality_Ensembles.
split; unfold Included, In, prop_ens; intuition.
change (prop_ens P tt = prop_ens Q tt). rewrite H0. auto.
Qed.

Lemma eq_implies_iff: forall (P Q:Prop), P = Q -> (P <-> Q).
intros. subst. intuition.
Qed.

Definition convertC: forall u (env:Env u) ty ty',
  (subE [|ty'|] (subE shsub env) , subTy [|ty'|] ty) = (env , subTy [|ty'|] ty).

intros. rewrite subE_ss, consmap_shsub, subE_idsub. auto.
Defined.
Implicit Arguments convertC [u env ty ty'].

Reserved Notation "e ~> e'" (at level 70, no associativity).
Inductive convert: forall u (env:Env u) ty, Exp env ty -> Exp env ty -> Prop :=

| c_app : forall u (env:Env u) ty ty' (e: Exp (ty'::env) ty) d,
  APP (LAM e) d ~> SubExp {| d |} e

| c_tapp : forall u (env:Env u) ty ty' (e: Exp (subE shsub env) ty),
  TAPP (TABS e) ty' ~> (<< SExp,PExp # convertC >> subExp [| ty' |] e)

| c_cong_lam : forall u (env:Env u) ty ty' (e e': Exp (ty'::env) ty),
  e ~> e' -> LAM e ~> LAM e'

| c_cong_app_1 : forall u (env:Env u) ty ty' (e e': Exp env (ty'--->ty)) d,
  e ~> e' -> APP e d ~> APP e' d

| c_cong_app_2 : forall u (env:Env u) ty ty' (e : Exp env (ty'--->ty)) d d',
  d ~> d' -> APP e d ~> APP e d'

| c_cong_tabs : forall u (env:Env u) ty (e e': Exp (subE shsub env) ty),
  e ~> e' -> TABS e ~> TABS e'

| c_cong_tapp : forall u (env:Env u) ty ty' (e e': Exp env (ALL ty)),
  e ~> e' -> TAPP e ty' ~> TAPP e' ty'

where "e ~> e'" := (convert e e').

Inductive SN u (env: Env u) ty: Exp env ty -> Prop :=
| sn_next: forall e, (forall e', e ~> e' -> SN e') -> SN e.

Definition normal u (env: Env u) ty (e: Exp env ty) : Prop :=
  forall e', ~ (e ~> e').

Definition neutral u (env: Env u) ty (e: Exp env ty) : Prop :=
  match e with
    | VAR _ _ => True
    | APP _ _ _ _ => True
    | TAPP _ _ _ => True
    | _ => False
  end.

Lemma convert_sub: forall u w (env : Env u) ty (s: subT u w) (e e': Exp env ty),
  e ~> e' -> subExp s e ~> subExp s e'.

intros. revert w s. induction H; intros; simpl.
  eapply eq_ind. apply c_app. rewrite subExp_SubExp, subSub_consMap, subSub_idSub. auto.

  rewrite (Hrf SExp PExp (subExp s _)). Hsimpl.
  ST_fold. Helimc C2.

  intros. eapply eq_ind. apply c_tapp.
  apply (Heq_eq SExp PExp). Hsimpl. do 2 Helimc.
  repeat rewrite (Hrw (subExp_ss _ _ _)). Hsimpl. rewrite sub_singsub. auto.

  apply c_cong_lam. apply IHconvert.
  apply c_cong_app_1. apply IHconvert.
  apply c_cong_app_2. apply IHconvert.
  apply c_cong_tabs. Hsimplc. apply IHconvert.
  Hsimplc. apply c_cong_tapp. apply IHconvert.
Qed.

Lemma convert_subst: forall u (env env': Env u) ty (Sub: SubT env env') (e e': Exp env ty),
  e ~> e' -> SubExp Sub e ~> SubExp Sub e'.

intros. revert env' Sub. induction H; intros; simpl.
  eapply eq_ind. apply c_app. rewrite SubExp_SS, SubExp_SS, Sub_singSub. auto.

  eapply eq_ind. apply c_tapp. apply (Heq_eq SExp PExp).
  rewrite subExp_SubExp. ST_fold. rewrite (Hrw (subSub_ss _ _ _)). Hsimpl.
  rewrite consmap_shsub. Hrewrite (subSub_idsub Sub). Hsimpl.
  Hrefl (Sub : SSub PSub) at 2. Helimc C0.
  Helimc C2. Hunify. auto.

  apply c_cong_lam. apply IHconvert.
  apply c_cong_app_1. apply IHconvert.
  apply c_cong_app_2. apply IHconvert.
  apply c_cong_tabs. apply IHconvert.
  apply c_cong_tapp. apply IHconvert.
Qed.

Definition Pred (A: Type) := A -> Prop.
Definition Rel (A B: Type) := A -> B -> Prop.

Definition simulation u (env: Env u) ty u' (env': Env u') ty'
  (R: Rel (Exp env ty) (Exp env' ty')) : Prop :=
  forall d e, R d e -> forall d', d ~> d' -> exists e', e ~> e' /\ R d' e'.

Lemma SN_by_simulation: forall u (env: Env u) ty u' (env': Env u') ty' (R: Rel (Exp env ty) (Exp env' ty')) d e,
  simulation R -> R d e -> SN e -> SN d.

intros. revert d H0. induction H1.
intros. apply sn_next; intros d' ?.
destruct (H _ _ H2 _ H3) as [e' [? ?]].
eapply H1. apply H4. assumption.
Qed.

Lemma SN_sub: forall u w env ty (s: subT u w) (tm: Exp env ty),
  SN (subExp s tm) -> SN tm.
intros.
set (SN_sub_rel := fun (e1: Exp env ty) e2 => e2 = subExp s e1).
assert (simulation SN_sub_rel).
  red; intros. unfold SN_sub_rel in H0. subst. unfold SN_sub_rel. exists (subExp s d'). split; auto.
  apply convert_sub. auto.
eapply (SN_by_simulation H0); [idtac | apply H]. unfold SN_sub_rel. auto.
Qed.

Lemma SN_subst: forall u (env env': Env u) ty (sub: SubT env env') (e: Exp env ty),
  SN (SubExp sub e) -> SN e.

intros. set (SN_subst_rel := fun (e1: Exp env ty) e2 => e2 = SubExp sub e1).
assert (simulation SN_subst_rel).
  red; intros. unfold SN_subst_rel in H0. subst. unfold SN_subst_rel. exists (SubExp sub d'). split; auto.
  apply convert_subst. auto.
eapply (SN_by_simulation H0); [idtac | apply H]. unfold SN_subst_rel. auto.
Qed.

Lemma SN_convert: forall u env ty (tm: @Exp u env ty) tm', tm ~> tm' -> SN tm -> SN tm'.
intros. destruct H0. apply H0. auto.
Qed.

Definition UnivVar u (env: Env u) := VarT env (ALL (TYVAR zVAR)).
Definition PredExp u (ty: Ty u) := forall env, UnivVar env -> Pred (Exp env ty).

Definition CR1 u (ty:Ty u) (R: PredExp ty) : Prop :=
  forall env uv e, R env uv e -> SN e.
Definition CR2 u (ty:Ty u) (R: PredExp ty) : Prop :=
  forall env uv e e', R env uv e -> e ~> e' -> R env uv e'.
Definition CR3 u (ty:Ty u) (R: PredExp ty) : Prop :=
  forall env uv e, neutral e -> (forall e', e ~> e' -> R env uv e') -> R env uv e.
Definition CR u (ty:Ty u) (R: PredExp ty) : Prop :=
  CR1 R /\ CR2 R /\ CR3 R.

Lemma CR4: forall u (ty:Ty u) (R: PredExp ty) env uv e,
  CR R -> neutral e -> normal e -> R env uv e.
intros. red in H; destr_pairs. apply H3; auto.
intros. absurd False; auto. apply (H1 e'). auto.
Qed.

Definition SNRC u (ty: Ty u) : PredExp ty := fun env uv => fun e => SN e.

Lemma SNRC_is_CR: forall u (ty: Ty u), CR (SNRC (ty:=ty)).

intros.
  split. red; intros. apply H.
  split. red; intros. destruct H. apply H. auto.
  red; intros. apply sn_next. intros. eapply H0. auto.
Qed.

Lemma SN_APP_1: forall u (env: Env u) ty1 ty2 (e: Exp env (ty1--->ty2)) d,
  SN (APP e d) -> SN e.

intros. set (SN_APP_rel := fun e1 e2 => e2 = APP (e1:Exp _ (_--->ty2)) d).
assert (simulation SN_APP_rel).
  red; intros. unfold SN_APP_rel in H0. subst. unfold SN_APP_rel. exists (APP d' d). split; auto.
  apply c_cong_app_1. auto.
eapply (SN_by_simulation H0); [idtac | apply H]. unfold SN_APP_rel. auto.
Qed.

Definition RC_arrow u (ty1 ty2:Ty u) (R: PredExp ty1) (S: PredExp ty2) : PredExp (ty1 ---> ty2) :=
  fun env uv e => forall e', R env uv e' -> S env uv (APP e e').

Lemma RC_arrow_is_CR: forall u (ty1 ty2:Ty u) (R: PredExp ty1) (S: PredExp ty2),
  CR R -> CR S -> CR (RC_arrow R S).

intros. red in H, H0; destr_pairs.

split.
  red; intros. apply SN_APP_1 with (TAPP (VAR uv) ty1). apply H0 with uv. apply H5.
  apply CR4. split; auto. simpl; auto.
  do 2 red; intros. dependent destruction H6. inversion H6.

split.
  do 2 red; intros. apply H2; simpl; auto. intros. apply H1 with (APP e' e'0).
  eapply H1. apply H5. apply H7. apply c_cong_app_1. auto. auto.

  do 2 red; intros.
  assertD (H _ _ _ H7). induction H8.
    apply H2. simpl; auto.
    intros. dependent destruction H10.
      inversion H5.
      apply H6. auto. auto.
      apply H9. auto. eapply H3. apply H7. auto.
Qed.

Definition PredExpList u w (U: subT u w) := forall (X: varT u), PredExp (U X).

Definition SPredExpList u w U := @PredExpList u w U.
Notation PPredExpList := (_) (only parsing).
Implicit Arguments SPredExpList [[u] [w]].

Definition varsp u (v: varT u) : varT (S (pred u)) :=
  match u as p return (varT p -> varT (S (pred p))) with
    | 0 => fun _ => zVAR
    | S _ => fun v => v
  end v.

Definition consPredExp u w (U: subT u w) ty (hd: PredExp ty) (tl: PredExpList U) : PredExpList (consmap ty U) :=
  fun (X: varT (S u)) =>
    match X in varT p return forall (U: subT (pred p) w), PredExp ty -> PredExpList U -> PredExp (consmap ty U (varsp X)) with
      | zVAR _ => fun U hd tl => hd
      | sVAR _ X' => fun U hd tl => tl X'
    end U hd tl.

Lemma consPredExp_hd: forall u w (U: subT u w) ty (hd: PredExp ty) (tl: PredExpList U), (consPredExp hd tl) zVAR = hd. auto. Qed.

Lemma consPredExp_tl: forall u w (U: subT u w) ty (hd: PredExp ty) (tl: PredExpList U) X, (consPredExp hd tl) (sVAR X) = tl X. auto. Qed.

Lemma consPredExp_is_CR: forall u w (U: subT u w) ty (hd: PredExp ty) (tl: PredExpList U),
  CR hd -> (forall X, CR (tl X)) -> forall X, CR (consPredExp hd tl (X:=X)).
intros. dependent destruction X. rewrite consPredExp_hd. auto. rewrite consPredExp_tl. apply (H0 X).
Qed.

Lemma REDC: forall u w (U: subT u w) (env:Env w) ty' ty,
  (env , subTy [|ty'|] (subTy (subL U) ty)) = (env , subTy (consmap ty' U) ty).
intros. rewrite subTy_ss, consmap_subL, idsub_ss. auto.
Qed.

Fixpoint RED u (ty: Ty u) w (U: subT u w) (R: PredExpList U) : PredExp (subTy U ty) :=
  match ty return PredExp (subTy U ty) with
    | TYVAR X => R X
    | ARR ty1 ty2 => RC_arrow (RED R) (RED R)
    | ALL ty0 => fun env uv e => forall ty' (Q: PredExp ty') C,
      CR Q -> RED (ty:=ty0) (consPredExp Q R) uv (<< SExp,PExp # C >> TAPP e ty' : SExp PExp)
  end.
Implicit Arguments RED [u w U env].

Ltac RST_fold := fold RED in *; ST_fold.

Lemma SN_TAPP: forall u (env: Env u) ty ty' (e: Exp env (ALL ty)),
  SN (TAPP e ty') -> SN e.
intros. set (SN_TAPP_rel := fun (e1:Exp env (ALL ty)) e2 => e2 = TAPP e1 ty').
assert (simulation SN_TAPP_rel).
  red; intros. unfold SN_TAPP_rel in H0. subst. unfold SN_TAPP_rel. exists (TAPP d' ty'). split; auto.
  apply c_cong_tapp. auto.
eapply (SN_by_simulation H0); [idtac | apply H]. unfold SN_TAPP_rel. auto.
Qed.

Lemma inv_convert_tapp: forall u (env:Env u) ty ty' (e: Exp env (ALL ty)) e',
  neutral e -> TAPP e ty' ~> e' -> exists e'', e ~> e'' /\ e' = TAPP e'' ty'.
intros.

inversion H0; Hsubst. contradiction. eexists. split. apply H5. auto.
Qed.

  (** Algorithm to improve "dependent destruction", discussed with Matthieu Sozeau. *)

  Definition TAPP_proj u (E:Env u) (T:Ty u) (e: Exp E T) : option {u : nat & ({E : Env u & ({T : Ty (S u) & {e : Exp E (ALL T) & Ty u } }) }) } :=
    match e with 
      | TAPP t e t' => Some ({{ _ # u, ({{ _ # E, ({{ _ # t, ({{ _ # e, t' }}) }}) }}) }})
      | _ => None
    end.

  Lemma TAPP_proj_cong: forall u (E:Env u) (T:Ty u) (e: Exp E T) u' (E':Env u') (T':Ty u') (e': Exp E' T'),
    {{{ u == u' }}} -> {{{ E == E' }}} -> {{{ T == T' }}} -> {{{ e == e' }}} -> TAPP_proj e = TAPP_proj e'.
  intros. Hsubst. auto.
  Qed.

  Lemma inv_convert_tapp': forall u (env:Env u) ty ty' (e: Exp env (ALL ty)) e',
    neutral e -> TAPP e ty' ~> e' -> exists e'', e ~> e'' /\ e' = TAPP e'' ty'.

  intros. 
  dependent destruction H0. 
  apply Heq_JMeq in H1. assert (H3:= TAPP_proj_cong (refl_Heq HId _ _) (refl_Heq HId _ _) (eq_HeqI H0) H1). 
    dependent destruction H3. contradiction.
  apply Heq_JMeq in H2. discriminate (TAPP_proj_cong (refl_Heq HId _ _) (refl_Heq HId _ _) (eq_HeqI H1) H2). 
  apply Heq_JMeq in H2. discriminate (TAPP_proj_cong (refl_Heq HId _ _) (refl_Heq HId _ _) (eq_HeqI H1) H2).
  apply Heq_JMeq in H2. assert (H4:= TAPP_proj_cong (refl_Heq HId _ _) (refl_Heq HId _ _) (eq_HeqI H1) H2). 
    dependent destruction H4. eexists. split; [ apply H0 | auto ].
  Qed.

Lemma RED_is_CR: forall u (ty: Ty u) w (U: subT u w) (R: PredExpList U),
  (forall X, CR (R X)) -> CR (RED ty R).

induction ty.
  intros. apply H.

  intros. apply RC_arrow_is_CR. apply IHty1; auto. apply IHty2; auto.

  intros.
  split.
  red; intros.
  apply SN_TAPP with (ALL (TYVAR zVAR)).
  simpl in H0. ST_fold. replace_hyp H0 (H0 (ALL (TYVAR zVAR)) (@SNRC _ _) (REDC _ _ _ _) (SNRC_is_CR _)).
  unfold CR in IHty; assertD (IHty _ _ _ (consPredExp_is_CR (SNRC_is_CR (ALL (TYVAR zVAR))) H)).
  apply H1 in H0.

  revert H0. Hsimplc. auto.

  split.
  do 2 red; intros. RST_fold.
  eapply (proj2m(IHty _ _ _ (consPredExp_is_CR H2 H))).
  apply (H0 _ Q C H2). Hsimplc.
  apply c_cong_tapp. apply H1.

  do 2 red; intros. RST_fold. apply (proj2(IHty _ _ _ (consPredExp_is_CR H2 H))).
  Hsimplc. simpl. auto.

  intros. revert H3. Hset_concl.
  Hsimpl. Hrefl (e': SExp PExp) at 1. Helimc C0.
  Hunset_concl.

  intros. destruct (inv_convert_tapp H0 H3) as [e'' [? ?]]. ST_fold.
  apply (eq_Heq SExp PExp) in H5. Hsimpl_hyps. Hrewrite H5. intros.
  apply (H1 _ H4). auto.
Qed.

Lemma RED_Hcong: forall u ty w U R e uv tm ty' U' R' e' uv' tm',
  ty = ty' -> U = U' -> {{ SVar,PVar # uv == uv' }} -> {{ SPredExpList,PPredExpList # R == R' }} -> {{ SExp,PExp # tm == tm' }} ->
  @RED u ty w U R e uv tm = @RED u ty' w U' R' e' uv' tm'.
intros. Hsubst. auto.
Qed.

Ltac assert_argtype f :=
  let tx := type of f in
    match tx with
      ?X -> _ => assert X
  end.

Lemma RED_renaming: forall u v w (V: renT u v) (W: subT v w) (R: PredExpList W) (env: Env w) uv (ty: Ty u)
  (e: Exp env (subTy W (subTy (rts V) ty))) (e': Exp env (subTy (W @ss@ (rts V)) ty)),
  {{SExp,PExp # e == e'}} -> (RED (subTy (rts V) ty) R uv e <-> RED ty (U:=W @ss@ (rts V)) (fun X => RED (rts V X) R) uv e').

intros until ty. revert v w V W R env uv. induction ty.

intros. simpl in *. Hsubst. intuition.

intros. assert ((env,subTy (W @ss@ rts V) ty1) = (env,subTy W (subTy (rts V) ty1))) by (rewrite subTy_ss; auto). rename H0 into Hc.
simpl in *. split; unfold RC_arrow; intros.
  apply (IHty2 _ _ _ _ _ _ _ (APP e (<< SExp,PExp # Hc >> e'0)) _).
  ST_fold. Hsimpl. Hrewritec H. auto.
  apply H0. assert ({{SExp,PExp # << SExp,PExp # Hc >> e'0 == e'0 }}) by (Hsimpl; auto).
  apply (IHty1 _ _ _ _ R _ _ _ _ H2). apply H1.

  apply (IHty2 _ _ _ _ _ _ _ _ (APP e' (<< SExp,PExp # sym_eq Hc>> e'0))).
  ST_fold. Hsimpl. Hrewritec <- H. auto.
  apply H0. assert ({{SExp,PExp # e'0 == << SExp,PExp # sym_eq Hc >> e'0 }}) by (Hsimpl; auto).
  apply (IHty1 _ _ _ _ R _ _ _ _ H2). apply H1.

intros. simpl in *. RST_fold. split; intros.
replace_hyp IHty (IHty _ _ (renL V) _ (consPredExp Q R) env uv).
assert_argtype (fun H => IHty (<< SExp,PExp # proj1 H >> TAPP e ty' : SExp PExp ) (<< SExp,PExp # proj2 H >> TAPP e' ty' : SExp PExp)).
  rewrite ! subTy_ss, ! consmap_subL, ! idsub_ss, ! rts_renL, ! consmap_subL. auto. destruct H2 as [C0 C1].
assert ({{SExp,PExp # << SExp,PExp # C0 >> TAPP e ty' == << SExp,PExp # C1 >> TAPP e' ty' }}).
  Hsimpl. Hrewritec H. auto.
erewrite RED_Hcong. apply (proj1 (IHty _ _ H2)). clear H2.
Hsimpl. rewrite rts_renL. intros. apply H0. auto. auto. mapext_destr. auto.
Hsplit. mapext_destr. apply Hfundep; auto. intros. Hsubst. red in a'. dependent destruction a'; auto. Hsimpl. auto.

replace_hyp IHty (IHty _ _ (renL V) _ (consPredExp Q R) env uv).
assert_argtype (fun H => IHty (<< SExp,PExp # proj1 H >> TAPP e ty' : SExp PExp) (<< SExp,PExp # proj2 H >> TAPP e' ty' : SExp PExp)).
  rewrite ! subTy_ss, ! consmap_subL, ! idsub_ss, ! rts_renL, ! consmap_subL. auto. destruct H2 as [C0 C1].
assert ({{SExp,PExp # << SExp,PExp # C0 >> TAPP e ty' == << SExp,PExp # C1 >> TAPP e' ty' }}).
  Hsimpl. Hrewritec H. auto.
erewrite RED_Hcong. apply (proj2 (IHty _ _ H2)). clear H2.
assert_argtype (fun x => H0 _ Q x). rewrite subTy_ss, consmap_subL, idsub_ss. auto.
erewrite RED_Hcong. apply (H0 _ Q H2 H1). auto. mapext_destr. auto.
Hsplit. mapext_destr. apply Hfundep. auto. intros. Hsubst. red in a'. dependent destruction a'; auto.
Hsimpl. auto. rewrite rts_renL. auto. auto. auto. auto. Hsimpl. auto.
Qed.

Lemma RED_substitution: forall u v w (V: subT u v) (W: subT v w) (R: PredExpList W)
  (env: Env w) uv (ty: Ty u) (e: Exp env (subTy W (subTy V ty))) (e': Exp env (subTy (W @ss@ V) ty)),
  {{SExp,PExp # e == e'}} -> (RED (subTy V ty) R uv e <-> RED ty (U:=W @ss@ V) (fun X => RED (V X) R) uv e').

intros until ty. revert v w V W R env uv. induction ty.

intros. simpl in *. Hsubst. intuition.

intros. assert ((env,subTy (W @ss@ V) ty1) = (env,subTy W (subTy V ty1))) by (rewrite subTy_ss; auto). rename H0 into Hc.
simpl in *. split; unfold RC_arrow; intros.
  apply (IHty2 _ _ _ _ _ _ _ (APP e (<< SExp,PExp # Hc >> e'0)) _).
  ST_fold. Hsimpl. Hrewritec H. auto.
  apply H0. assert ({{SExp,PExp # << SExp,PExp # Hc >> e'0 == e'0 }}) by (Hsimpl; auto).
  apply (IHty1 _ _ _ _ R _ _ _ _ H2). apply H1.

  apply (IHty2 _ _ _ _ _ _ _ _ (APP e' (<<SExp,PExp # sym_eq Hc>> e'0))).
  ST_fold. Hsimpl. Hrewritec <- H. auto.
  apply H0. assert ({{SExp,PExp # e'0 == << SExp,PExp # sym_eq Hc >> e'0 }}) by (Hsimpl; auto).
  apply (IHty1 _ _ _ _ R _ _ _ _ H2). apply H1.

intros. simpl in *. RST_fold. split; intros.
replace_hyp IHty (IHty _ _ (subL V) _ (consPredExp Q R) env uv ).
assert_argtype (fun H => IHty (<< SExp,PExp # proj1 H >> TAPP e ty' : SExp PExp) (<< SExp,PExp # proj2 H >> TAPP e' ty' : SExp PExp)).
  rewrite ! subTy_ss, ! consmap_subL, ! idsub_ss. auto. destruct H2 as [C0 C1].
assert ({{SExp,PExp # << SExp,PExp # C0 >> TAPP e ty' == << SExp,PExp # C1 >> TAPP e' ty' }}).
  Hsimpl. Hrewritec H. auto.
erewrite RED_Hcong. apply (proj1 (IHty _ _ H2)). clear H2.
  apply H0. auto. auto. rewrite consmap_subL. auto. auto.
Hsplit. rewrite consmap_subL. auto.
  apply Hfundep; auto. intros. Hsubst. red in a'. dependent destruction a'. auto.
    rewrite consPredExp_tl. apply sym_Heq.
      apply Hfundep; auto; intros; Hsubst.
      apply Hfundep; auto; intros; Hsubst.
      apply Hfun. simpl. rewrite consmap_subL. auto. simpl. unfold scs, subL. rewrite renTy_def.
        intros. red in a'0, a'1, a, a'2. rename a' into var', a'0 into env', a'1 into uv'.
        apply eq_Heq. apply iff_implies_eq.
        assert (C3:(env', subTy (consmap ty' W) (subTy (rts shren) (V var')))=(env', subTy (consmap ty' W @ss@ rts shren) (V var'))).
          rewrite subTy_ss. auto.
        eapply iff_trans. apply (@RED_renaming _ _ _ _ _ _ _ _ _ _ (<<SExp,PExp # C3>> a )). Hsimpl. auto.
        eapply eq_ind. apply iff_refl. apply RED_Hcong. auto. mapext_destr. auto.
        Hsplit. mapext_destr. apply Hfundep. auto. intros. red in a0, a'. Hsubst. dependent destruction a'; auto.
        Hsimpl. Hsplit. rewrite subTy_ss, consmap_shsub. auto. auto. Hsimpl. auto.

replace_hyp IHty (IHty _ _ (subL V) _ (consPredExp Q R) env uv ).
assert_argtype (fun H => IHty (<< SExp,PExp # proj1 H >> TAPP e ty' : SExp PExp) (<< SExp,PExp # proj2 H >> TAPP e' ty' : SExp PExp)).
  rewrite ! subTy_ss, ! consmap_subL, ! idsub_ss. auto. destruct H2 as [C0 C1].
assert ({{SExp,PExp # << SExp,PExp # C0 >> TAPP e ty' == << SExp,PExp # C1 >> TAPP e' ty' }}).
  Hsimpl. Hrewritec H. auto.
erewrite RED_Hcong. apply (proj2 (IHty _ _ H2)). clear H2.
  assert_argtype (fun H => H0 ty' Q H). rewrite subTy_ss, consmap_subL, idsub_ss. auto.
erewrite RED_Hcong. apply (H0 ty' Q H2 H1). auto. rewrite consmap_subL. auto. auto.
  Hsplit. rewrite consmap_subL. auto. apply Hfundep. auto. intros. Hsubst. red in a'. dependent destruction a'; auto.
    rewrite consPredExp_tl. apply sym_Heq.
      apply Hfundep; auto; intros; Hsubst.
      apply Hfundep; auto; intros; Hsubst.
      apply Hfun. simpl. rewrite consmap_subL. auto. simpl. unfold scs, subL. rewrite renTy_def.
        intros. red in a'0, a'1, a, a'2. rename a' into var', a'0 into env', a'1 into uv'.
        apply eq_Heq. apply iff_implies_eq.
      assert ((env', subTy (consmap ty' W) (subTy shsub (V var')))=(env', subTy (consmap ty' W @ss@ rts shren) (V var')))
        by (rewrite subTy_ss; auto).
      apply iff_sym. eapply iff_trans. apply (@RED_renaming _ _ _ shren _ (consPredExp Q R) _ _ _ _ (<<SExp,PExp # H3>> a'2 )). Hsimpl. auto.
        eapply eq_ind. apply iff_refl. apply RED_Hcong. auto. mapext_destr. auto.
        Hsplit. mapext_destr. apply Hfundep. auto. intros. red in a0, a'. Hsubst. dependent destruction a'; auto.
        Hsimpl. Hsplit. rewrite subTy_ss, consmap_shsub. auto. apply sym_Heq. auto. Hsimpl. auto.

auto. auto. auto. auto. Hsimpl. auto.
Qed.

Lemma RED_LAM: forall u v (W: subT u v) (R: PredExpList W) (env: Env v) uv ty1 ty2 (tm: Exp (subTy W ty1::env) (subTy W ty2)),
  (forall X, CR (R X)) -> (forall tm', RED ty1 R uv tm' -> RED ty2 R uv (SubExp {|tm'|} tm)) -> RED (ty1--->ty2) R uv (LAM tm).

intros. simpl. unfold RC_arrow; intros.
assertD (proj1(RED_is_CR _ H) _ uv _ H1).
assertD (SN_subst (proj1(RED_is_CR _ H) _ uv _ (H0 _ H1))).
induction H3. induction H2.
  eapply (proj3(RED_is_CR _ H)). simpl. auto.
  intros. inversion H6; Hsubst. apply H0. auto.
  inversion H11; Hsubst.
    apply H4. auto. intros. eapply (proj2m(RED_is_CR _ H)). apply H0. apply H7. apply convert_subst. auto.
    apply H5. auto. eapply (proj2m(RED_is_CR _ H)). apply H1. auto.
      intros. eapply (proj2m(RED_is_CR _ H)). apply H4. apply H7. apply H8. apply c_cong_app_2. auto.
Qed.

Lemma REDC2: forall u v (env: Env v) (W:subT u v) ty ty',
  (env, subTy [|ty'|] (subTy (subL W) ty)) = (env, (subTy (consmap ty' W) ty)).
intros. rewrite subTy_ss. rewrite consmap_subL. rewrite idsub_ss. auto.
Qed.
Implicit Arguments REDC2 [[u] [v] [env] [W] [ty] [ty']].

Lemma RED_TABS: forall u v (W: subT u v) (R: PredExpList W) env (uv:UnivVar env) ty (tm: Exp (subE shsub env) (subTy (subL W) ty)),
  (forall X, CR (R X)) ->
  (forall ty' (Q: PredExp ty'),
    CR Q -> RED ty (consPredExp Q R) (subVar _ (subVar _ uv)) (<< SExp,PExp # REDC2 >> subExp [|ty'|] tm)) ->
  RED (ALL ty) R uv (TABS tm).

intros.
assertD (proj1 (RED_is_CR ty (consPredExp_is_CR (SNRC_is_CR _) H)) _ _ _ (H0 _ _ (SNRC_is_CR (ALL (TYVAR zVAR))))).
revert H1. Hsimplc. intros.
assert (H2:= SN_sub H1); clear H1.
revert H0. induction H2; intros.
  unfold RED; fold RED subTy; intros.
  apply (proj3(RED_is_CR ty (consPredExp_is_CR H3 H))).
  Hsimplc. simpl; auto.
  intros. revert H4. Hsimpl. Hrefl (e':SExp PExp) at 1.
Helimc C0. intros.
  inversion H4; Hsubst.
    apply (eq_Heq SExp PExp) in H17. Hsimpl_hyps.
    erewrite RED_Hcong. apply (H2 _ Q H3).
    auto. auto. rewrite (Hrw (subVar_ss _ _ _)); Hsimpl. apply sym_Heq, subVar_idsub. auto. Hsimpl. apply sym_Heq, H17.

    inversion H9; Hsubst.
    assert (RED (ALL ty) R uv (TABS e'1)).
      apply (H1 _ H10).
      intros. assertD (H2 _ Q0 H5).
      eapply (proj2m (RED_is_CR ty (consPredExp_is_CR H5 H))). apply H6.
      Hsimplc.
      apply convert_sub. auto.

    red in H5. RST_fold. eapply eq_ind. apply (H5 _ Q REDC2 H3).
    apply (Heq_eq SExp PExp). rewrite H16. Hsimpl. auto.
Qed.

Lemma REDC3: forall u v (W: subT u v) (env: Env v) (ty: Ty (S u)) (ty': Ty u),
  (env, subTy [|subTy W ty'|] (subTy (subL W) ty)) = (env, subTy W (subTy [|ty'|] ty)).
intros. repeat rewrite subTy_ss. rewrite sub_singsub. auto.
Qed.

Lemma RED_TAPP: forall u v (W: subT u v) (R: PredExpList W) env ty (tm: Exp env (subTy W (ALL ty))) ty' uv,
  (forall X, CR (R X)) ->
  RED (ALL ty) R uv tm -> RED (subTy [|ty'|] ty) R uv (<< SExp,PExp # REDC3 _ _ _ _ >> TAPP tm (subTy W ty')).

intros. unfold RED in H0; RST_fold.
replace_hyp H0 (H0 _ (RED ty' R) (REDC _ _ _ _) (RED_is_CR _ H)).
assert ((env, (subTy [|subTy W ty'|] (subTy (subL W) ty)))=(env, (subTy (W @ss@ [|ty'|]) ty))) by (rewrite subTy_ss, sub_singsub; auto).
apply (@RED_substitution _ _ _ _ _ _ _ _ _ _ (<< SExp,PExp # H1 >> TAPP tm (subTy W ty'))). Hsimpl. auto.
erewrite RED_Hcong. apply H0. auto. auto. rewrite sub_singsub, consmap_subL, idsub_ss. auto. auto.
Hsplit. rewrite sub_singsub, consmap_subL, idsub_ss. auto.
apply Hfundep; auto. intros. Hsubst. apply Hfundep; auto. intros. Hsubst.
red in a'. dependent destruction a'.
  rewrite consPredExp_hd. auto.
  rewrite consPredExp_tl. auto.
Hsimpl. auto.
Qed.

Theorem Fundamental: forall u (env: Env u) ty (tm: Exp env ty) v (W: subT u v) (R: PredExpList W) env' (uv:UnivVar _) (sub: SubT _ (subE W env')),
  (forall X, CR (R X)) -> (forall t (var: VarT env t), RED t R (subVar _ uv) (sub _ (subVar W var)))
  -> RED ty R (subVar _ uv) (SubExp sub (subExp W tm)).

induction tm; intros.

simpl. apply H0.

simpl subExp. simpl SubExp. RST_fold. apply RED_LAM. apply H.
intros. rewrite SubExp_SS, consMap_SubL, idSub_SS. apply IHtm. auto.
intros. dependent destruction var. simpl. auto. simpl. auto.

simpl subExp. simpl SubExp.
assert (RED _ R (subVar _ uv) (SubExp sub (subExp W tm1))). apply IHtm1; auto.
assert (RED _ R (subVar _ uv) (SubExp sub (subExp W tm2))). apply IHtm2; auto.
apply H1. RST_fold. apply H2.

simpl subExp. simpl SubExp. apply RED_TABS. auto.
intros. rewrite subExp_SubExp. RST_fold. Hrewrite (subSub_ss [|ty'|] shsub sub). Hsimpl.
rewrite ! consmap_shsub. Hrewrite (subSub_idsub sub). Hsimpl. Helimc C0.
Hrewritec (subExp_ss [|ty'|] (subL W) tm). rewrite consmap_subL, idsub_ss. Hclear.
assert (C: (subE W E, subE W env') = (subE (consmap ty' W) (subE shsub E), subE (consmap ty' W) (subE shsub env'))).
  repeat rewrite subE_ss. rewrite consmap_shsub. auto. intros.

erewrite RED_Hcong.
apply (IHtm _ _ (consPredExp Q R) _ (subVar _ uv) (<< SSub,PSub # C >> sub) (consPredExp_is_CR H1 H)).
  intros. destruct (Var_inv var) as [t' [var' [? ?]]]. Hsubst.
  assert (C1: (subE W env', subTy W t')=(subE (consmap ty' W) (subE shsub env'), subTy (consmap ty' W @ss@ shsub) t')).
    rewrite subE_ss, consmap_shsub. auto.
  apply (@RED_substitution _ _ _ _ _ _ _ _ _ _ (<< SExp,PExp # C1 >> sub _ (subVar W var'))).
  Hrewritec (subVar_ss (consmap ty' W) shsub var'). Helimc. rewrite ! consmap_shsub. Hclear. auto.

erewrite RED_Hcong. apply (H0 _ var').
  auto. rewrite consmap_shsub. auto.
  Hrewritec (subVar_ss (consmap ty' W) shsub uv). rewrite consmap_shsub. auto.
Hsplit. rewrite consmap_shsub. auto.
  apply Hfundep; auto. intros. Hsubst. red in a'. rewrite <- (consPredExp_tl Q R). auto.
Hsimpl. auto. auto. auto.
Hrewritec (subVar_ss shsub W uv).
rewrite (Hrw (subVar_ss [|ty'|] _ uv)), (Hrw (subVar_ss _ shsub uv)). Hsimpl.
  rewrite <- sss_assoc, ! consmap_shsub, idsub_ss. auto.
auto. Hsimpl. Helim. Helim C2. Hunify. auto.

simpl subExp. Hrewrite (SubExp_subExp_TAPP tm t' sub). RST_fold.
intros. Hchange C with (REDC3 W (subE W env') t t'). apply RED_TAPP. auto.
apply IHtm. auto. auto.
Qed.

Corollary StrongNormalization: forall u (env: Env u) ty (tm: Exp env ty), SN tm.

intros. eapply SN_subst. instantiate (1:= shSub (ALL (TYVAR zVAR))).
assert (RED _ (U:=idsub) (fun X => @SNRC u (TYVAR X)) (ZVAR _ _) (subExp idsub (SubExp (shSub (ALL (TYVAR zVAR))) tm))).
  RST_fold. erewrite RED_Hcong.
  apply (@Fundamental _ _ _ (SubExp (shSub (ALL (TYVAR zVAR))) tm) u
         idsub (fun X => @SNRC _ (TYVAR X)) _ (ZVAR _ _) idSub (fun X => SNRC_is_CR (TYVAR X))).
  intros. apply CR4. apply RED_is_CR. intro; apply SNRC_is_CR. simpl. auto. simpl. auto. do 2 red; intros; inversion H.
  auto. auto. auto. auto.
  rewrite subExp_SubExp, SubExp_SS, idSub_SS. auto.
  replace_hyp H (proj1(@RED_is_CR _ _ _ idsub _ (fun X => SNRC_is_CR (TYVAR X))) _ _ _ H).
  apply (SN_sub (s:= idsub)). auto.
Qed.