Commits

Paweł Wieczorek committed 7b271b8

Specialized directory for LogRelSb

Comments (0)

Files changed (15)

 Nbe/Model/LogRelTm/Lift.v
 Nbe/Model/LogRelTm/Back.v
 Nbe/Model/LogRelTm.v
-Nbe/Model/LogRelSb_Def.v
-Nbe/Model/LogRelSb_BasicFacts.v
-Nbe/Model/LogRelSb_Fundamental_Helpers.v
-Nbe/Model/LogRelSb_Fundamental_WIP.v
-Nbe/Model/LogRelSb_Fundamental.v
-Nbe/Model/LogRelSb_Id.v
+Nbe/Model/LogRelSb/Def.v
+Nbe/Model/LogRelSb/BasicFacts.v
+Nbe/Model/LogRelSb/Fundamental/Helpers.v
+Nbe/Model/LogRelSb/Fundamental/WIP.v
+Nbe/Model/LogRelSb/Fundamental.v
+Nbe/Model/LogRelSb/Id.v
 Nbe/Model/LogRelSb.v
 Nbe/Model/LogRel.v
 Nbe/Model/Final.v
   Nbe/Model/LogRelTm/Lift.v\
   Nbe/Model/LogRelTm/Back.v\
   Nbe/Model/LogRelTm.v\
-  Nbe/Model/LogRelSb_Def.v\
-  Nbe/Model/LogRelSb_BasicFacts.v\
-  Nbe/Model/LogRelSb_Fundamental_Helpers.v\
-  Nbe/Model/LogRelSb_Fundamental_WIP.v\
-  Nbe/Model/LogRelSb_Fundamental.v\
-  Nbe/Model/LogRelSb_Id.v\
+  Nbe/Model/LogRelSb/Def.v\
+  Nbe/Model/LogRelSb/BasicFacts.v\
+  Nbe/Model/LogRelSb/Fundamental/Helpers.v\
+  Nbe/Model/LogRelSb/Fundamental/WIP.v\
+  Nbe/Model/LogRelSb/Fundamental.v\
+  Nbe/Model/LogRelSb/Id.v\
   Nbe/Model/LogRelSb.v\
   Nbe/Model/LogRel.v\
   Nbe/Model/Final.v\

Nbe/Model/LogRelSb.v

  * Pawel Wieczorek
  *)
 
-Require Export Nbe.Model.LogRelSb_Def.
-Require Export Nbe.Model.LogRelSb_BasicFacts.
-Require Export Nbe.Model.LogRelSb_Fundamental_Helpers.
-Require Export Nbe.Model.LogRelSb_Fundamental.
-Require Export Nbe.Model.LogRelSb_Id.
+Require Export Nbe.Model.LogRelSb.Def.
+Require Export Nbe.Model.LogRelSb.BasicFacts.
+Require Export Nbe.Model.LogRelSb.Fundamental.Helpers.
+Require Export Nbe.Model.LogRelSb.Fundamental.
+Require Export Nbe.Model.LogRelSb.Id.

Nbe/Model/LogRelSb/BasicFacts.v

+
+(******************************************************************************
+ * Pawel Wieczorek
+ *)
+
+Set Implicit Arguments.
+
+(*
+Add Rec LoadPath "../../Nbe" as Nbe.
+ *)
+
+
+Require Import Arith.
+Require Import Arith.Plus.
+
+Require Import Program.
+Require Import Program.Tactics.
+Require Import Program.Equality.
+Require Import Setoid.
+Require Import Relations.Relation_Definitions.
+Require Import Classes.RelationClasses.
+Add Rec LoadPath "../../Nbe" as Nbe.
+
+
+Require Import Nbe.Syntax.
+Require Import Nbe.Domain.
+Require Import Nbe.Utils.
+Require Import Nbe.Model.PER.
+Require Import Nbe.Model.Interp.
+Require Import Nbe.Model.Valid.
+Require Import Nbe.Model.Terminating.
+Require Import Nbe.Model.LogRelTm.
+Require Import Nbe.Model.LogRelSb.Def.
+
+
+(******************************************************************************
+ * Basic Properties
+ *)
+
+Lemma RelSb_wellformed: forall Gamma sb Delta denv,
+  Gamma ||- [sb] : Delta #aeq# denv ->
+  Gamma |-- [sb] : Delta
+.
+Proof.
+intros.
+clear_inversion H; eauto.
+Qed.
+
+Lemma RelSb_valenv: forall Gamma sb Delta denv,
+  Gamma ||- [sb] : Delta #aeq# denv ->
+  [denv] === [denv] #in# Delta
+.
+Proof.
+intros.
+induction H; auto.
+econstructor 2; eauto.
+red.
+eexists; eauto.
+Qed.
+
+(******************************************************************************
+ * Closed under sb equality
+ *)
+
+Lemma RelSb_ClosedUnderEq: forall Gamma sb1 sb2 Delta denv,
+  Gamma |-- [sb1] === [sb2] : Delta ->
+  Gamma ||- [sb1] : Delta #aeq# denv ->
+  Gamma ||- [sb2] : Delta #aeq# denv
+.
+Proof.
+intros.
+induction H0.
+constructor 1; eauto.
+(**)
+econstructor 2; eauto.
+Qed.
+
+(******************************************************************************
+ * Helper: closed under one lifting
+ *)
+
+Lemma RelSb_lift1: forall Gamma sb Delta denv A,
+  Gamma ||- [sb] : Delta #aeq# denv ->
+  Gamma |-- A ->
+  Gamma,,A ||- [Sseq sb Sup] : Delta #aeq# denv
+.
+Proof.
+intros.
+induction H.
+constructor 1.
+eauto.
+(*-*)
+assert (Gamma |-- [sb] : Delta).
+eapply RelSb_wellformed; eauto.
+
+assert (Gamma |-- [Sext sb M] : Delta,,A0).
+eauto.
+clear_inversion H9.
+
+econstructor 2; eauto. 
+eapply RelType_ClosedForConversion with (T := TmSb (TmSb A0 sb) Sup).
+eapply RelTypeLift1.
+eauto.
+auto.
+(**)
+eapply EQ_TP_SBSEQ; eauto.
+(**)
+eapply RelTerm_ClosedForConversion with (T := TmSb (TmSb A0 sb) Sup) (t := TmSb M Sup).
+eapply RelTypeLift1.
+eauto.
+auto.
+eapply EQ_TP_SBSEQ; eauto.
+(**)
+eapply RelTermLift1.
+eauto.
+auto.
+eauto.
+(**)
+eapply EQ_SB_TRANS.
+eapply EQ_SB_CONG_SSEQ.
+eauto.
+apply H3.
+eauto.
+Qed.
+
+Lemma RelSb_lift1_left: forall Gamma sb Delta denv dt A,
+  Gamma ||- [sb] : Delta,,A #aeq# (Dext denv dt) ->
+  Delta |-- A ->
+  Gamma ||- [Sseq Sup sb] : Delta #aeq# denv
+.
+Proof.
+intros. 
+clear_inversion H.
+rename sb into SB.
+rename sb0 into sb.
+
+assert (Gamma |-- [sb] : Delta).
+eapply RelSb_wellformed; eauto.
+
+assert (Gamma |-- [Sext sb M] : Delta,,A).
+eauto.
+
+clear_inversion H1.
+
+eapply RelSb_ClosedUnderEq.
+eapply EQ_SB_SYM.
+eapply EQ_SB_TRANS.
+eapply EQ_SB_CONG_SSEQ.
+eauto.
+eauto.
+eapply EQ_SB_SUP.
+eauto.
+eauto.
+eauto.
+auto.
+Qed.
+
+(******************************************************************************
+ * Closed under lifting
+ *)
+
+Lemma RelSb_ClosedUnderLift: forall Gamma sb Delta denv,
+  Gamma ||- [sb] : Delta #aeq# denv -> forall Psi i, CxtShift Psi i Gamma -> 
+    Psi ||- [Sseq sb (Sups i)] : Delta #aeq# denv
+.
+Proof.
+(**)
+intros.
+red in H0.
+generalize dependent Gamma.
+generalize dependent sb.
+generalize dependent Delta.
+generalize dependent denv.
+generalize dependent Psi.
+induction i; intros.
+(**)
+simpl in *.
+clear_inversion H0.
+eapply RelSb_ClosedUnderEq.
+eapply EQ_SB_SYM.
+eapply EQ_SB_SIDR.
+eauto using RelSb_wellformed.
+auto.
+(**)
+simpl in *.
+edestruct WtSb_SUPL with (Gamma := Psi) as [Theta [A [HTheta HA] ]]; eauto.
+subst.
+specialize (IHi Theta denv Delta).
+specialize (IHi sb Gamma H).
+specialize (IHi HA).
+
+eapply RelSb_ClosedUnderEq.
+eapply EQ_SB_COMM.
+eapply SUP.
+assert (Theta,,A |--) by eauto.
+clear_inversion H1.
+auto.
+
+eauto.
+eapply RelSb_wellformed; eauto.
+
+apply RelSb_lift1.
+auto.
+assert (Theta,,A |--) by eauto.
+clear_inversion H1.
+auto.
+Qed.
+
+(******************************************************************************
+ * 
+ *)
+
+Lemma ValEnv_interp: forall A Gamma denv denv' PA,
+  Gamma |-- A ->
+  InterpTypePer A denv PA ->
+  [denv] === [denv'] #in# Gamma ->
+  InterpTypePer A denv' PA
+.
+Proof.
+intros.
+assert (Gamma |= A).
+apply Valid_for_WfTp; auto.
+clear_inversion H2.
+edestruct H4 as [DA [DB]].
+eauto.
+program_simpl.
+red.
+exists DB; split; auto.
+red in H0.
+destruct H0.
+destruct H0.
+compute_sth.
+Qed.
+
+(******************************************************************************
+ * Closed under valid environments
+ *)
+
+(* 
+Theorem RelSb_ClosedUnderValEnv: forall Gamma sb Delta denv denv',
+  Gamma ||- [sb] : Delta #aeq# denv ->
+  [denv] === [denv'] #in# Delta ->
+  Gamma ||- [sb] : Delta #aeq# denv'
+.
+Proof.
+
+intros until denv'.
+intro H.
+generalize dependent denv'.
+induction H; intros.
+clear_inversion H0.
+eauto.
+(**) 
+clear_inversion H7.
+econstructor 2; eauto.
+
+red in H14.
+destruct H14.
+destruct H7.
+renamer.
+ 
+eapply RelTerm_ClosedUnderPer'; eauto.
+elim_deters.
+
+(**)
+ 
+specialize (IHRelSb _ H3).
+assert (PER (ValEnv Delta)).
+apply ValEnv_is_Per.
+apply Valid_for_WfCxt.
+eapply WfSbCxt_from_WtSb.
+eapply WtSb_from_WtSbEq2.
+eapply EQ_SB_REFL.
+eapply RelSb_wellformed.
+eauto.
+
+apply PER_Transitive with denv.
+symmetry; auto.
+eauto.
+
+(**)
+
+destruct H14.
+program_simpl; renamer.
+elim_deters.
+clear_dups.
+
+rename DA_denv0 into DX.
+
+
+dmit.
+
+(**)
+
+destruct H14.
+program_simpl; renamer.
+elim_deters.
+clear_dups.
+find_extdeters.
+
+assert (PER PDA_denv0).
+eapply Interp_pers.
+eauto.
+
+assert (PER PDA_denv).
+eapply Interp_pers.
+eauto.
+
+eapply PER_Transitive with dM; auto.
+symmetry; eauto.
+apply H7.
+apply H15.
+apply H7.
+apply H15.
+
+Qed.
+*)
+
+
+Lemma EQ_TP_SB_ARR: forall Gamma Delta A B sb,
+  Gamma |-- [sb] : Delta ->
+  Delta |-- A ->
+  Delta |-- B ->
+  Gamma |-- TmSb (TmArr A B) sb === TmArr (TmSb A sb) (TmSb B sb)
+.
+Proof.
+intros.
+unfold TmArr.
+eapply EQ_TP_TRANS.
+ 
+eapply EQ_TP_SB_FUN.
+eauto.
+eauto.
+eauto.
+
+eapply EQ_TP_CONG_FUN.
+eauto.
+
+eapply EQ_TP_SYM.
+eapply EQ_TP_TRANS.
+eapply EQ_TP_SBSEQ.
+eauto.
+eauto.
+eauto.
+eapply EQ_TP_SYM.
+eapply EQ_TP_TRANS.
+eapply EQ_TP_SBSEQ.
+eapply SEXT.  
+eauto.
+eapply H0.
+eapply CONV.
+eapply HYP.
+eapply EXT.
+eauto.
+eapply SB_F.
+eauto.
+eauto.
+eapply EQ_TP_SBSEQ.
+eauto.
+eauto.
+eauto.
+eauto.
+eauto.
+eapply EQ_TP_CONG_SB.
+eapply EQ_SB_TRANS.
+eapply EQ_SB_SUP.
+eauto.
+eapply H0.
+eapply CONV.
+eapply HYP.
+eapply EXT.
+eauto.
+eauto.
+eapply EQ_TP_SBSEQ.
+eauto.
+eauto.
+eauto.
+eauto.
+eauto.
+
+eapply EQ_TP_SYM.
+eapply EQ_TP_TRANS.
+eapply EQ_TP_SBSEQ.
+eauto.
+eauto.
+eauto.
+eapply EQ_TP_SYM.
+eapply EQ_TP_TRANS.
+eapply EQ_TP_SBSEQ.
+eapply SEXT.  
+eauto.
+eapply H0.
+eapply CONV.
+eapply HYP.
+eapply EXT.
+eauto.
+eapply SB_F.
+eauto.
+eauto.
+eapply EQ_TP_SBSEQ.
+eauto.
+eauto.
+eauto.
+eauto.
+eauto.
+eapply EQ_TP_CONG_SB.
+eapply EQ_SB_TRANS.
+eapply EQ_SB_SUP.
+eauto.
+eapply H0.
+eapply CONV.
+eapply HYP.
+eapply EXT.
+eauto.
+eauto.
+eapply EQ_TP_SBSEQ.
+eauto.
+eauto.
+eauto.
+eauto.
+eauto.
+Qed.
+
+

Nbe/Model/LogRelSb/Def.v

+
+(******************************************************************************
+ * Pawel Wieczorek
+ *)
+
+Set Implicit Arguments.
+
+(*
+Add Rec LoadPath "../../Nbe" as Nbe.
+ *)
+
+
+Require Import Arith.
+Require Import Arith.Plus.
+
+Require Import Program.
+Require Import Program.Tactics.
+Require Import Program.Equality.
+Require Import Setoid.
+Require Import Relations.Relation_Definitions.
+Require Import Classes.RelationClasses.
+Add Rec LoadPath "../../Nbe" as Nbe.
+
+
+Require Import Nbe.Syntax.
+Require Import Nbe.Domain.
+Require Import Nbe.Utils.
+Require Import Nbe.Model.PER.
+Require Import Nbe.Model.Interp.
+Require Import Nbe.Model.Valid.
+Require Import Nbe.Model.Terminating.
+Require Import Nbe.Model.LogRelTm.
+
+(*****************************************************************************)
+(*****************************************************************************)
+(*****************************************************************************)
+(******************************************************************************
+ * Relations for substitutions
+ *)
+
+Reserved Notation "Gamma ||- [ s ] : Delta #aeq# env"
+ (no associativity, at level 75, A, X, t, d at next level).
+
+
+Inductive RelSb : Cxt -> Sb -> Cxt -> DEnv -> Prop :=
+  | RelSb_Sid: forall Gamma sb,
+    Gamma |-- [ sb ] : nil ->
+    Gamma ||- [ sb ] : nil #aeq# Did
+
+ |  RelSb_Sext: forall Gamma Delta A M SB sb denv dM DX DX' (HDX : DX === DX' #in# PerType) PX,
+   Gamma ||- [ sb ] : Delta #aeq# denv ->
+   Gamma ||- TmSb A sb #in# HDX ->
+   Gamma ||- M : TmSb A sb #aeq# dM #in# HDX ->
+   Gamma |-- [ SB ] === [Sext sb M ] : Delta,,A ->
+   [denv] === [denv] #in# Delta ->
+   EvalTm A denv DX ->
+   Interp DX PX ->
+   dM === dM #in# PX ->
+   Gamma ||- [ SB ] : Delta,,A #aeq# Dext denv dM
+    
+where "Gamma ||- [ s ] : Delta #aeq# denv" := (RelSb Gamma s Delta denv)
+.
+Hint Constructors RelSb.
+

Nbe/Model/LogRelSb/Fundamental.v

+
+(******************************************************************************
+ * Pawel Wieczorek
+ *)
+
+Set Implicit Arguments.
+
+(*
+Add Rec LoadPath "../../Nbe" as Nbe.
+ *)
+
+
+Require Import Arith.
+Require Import Arith.Plus.
+
+Require Import Program.
+Require Import Program.Tactics.
+Require Import Program.Equality.
+Require Import Setoid.
+Require Import Relations.Relation_Definitions.
+Require Import Classes.RelationClasses.
+Add Rec LoadPath "../../Nbe" as Nbe.
+
+
+Require Import Nbe.Syntax.
+Require Import Nbe.Domain.
+Require Import Nbe.Utils.
+Require Import Nbe.Model.PER.
+Require Import Nbe.Model.Interp.
+Require Import Nbe.Model.Valid.
+Require Import Nbe.Model.Terminating.
+Require Import Nbe.Model.LogRelTm.
+Require Import Nbe.Model.LogRelSb.Def.
+Require Import Nbe.Model.LogRelSb.BasicFacts.
+Require Import Nbe.Model.LogRelSb.Fundamental_Helpers.
+Require Import Nbe.Model.LogRelSb.Fundamental_WIP.
+
+
+Theorem Rel_Fundamental: 
+    (forall Gamma, Gamma |-- -> True) /\
+
+    (forall Gamma T, Gamma |-- T ->
+      forall Delta SB denv,
+      Delta ||- [SB] : Gamma #aeq# denv -> 
+        forall DT DT', forall HDT : DT === DT' #in# PerType,
+          EvalTm T denv DT ->
+          Delta ||- TmSb T SB #in# HDT
+    ) /\    
+
+    (forall Gamma t T, Gamma |-- t : T -> 
+      forall Delta SB denv,
+      Delta ||- [SB] : Gamma #aeq# denv -> 
+        forall DT DT', forall HDT : DT === DT' #in# PerType, forall dt,
+          EvalTm T denv DT ->
+          EvalTm t denv dt ->
+          Delta ||- TmSb t SB : TmSb T SB #aeq# dt #in# HDT
+    ) /\    
+
+    (forall Gamma sb Psi, Gamma |-- [sb] : Psi ->
+      forall Delta SB denv,
+      Delta ||- [SB] : Gamma #aeq# denv -> 
+       forall dsb,
+         EvalSb sb denv dsb ->
+         Delta ||- [Sseq sb SB] : Psi #aeq# dsb
+    ) /\    
+
+    (forall Gamma T1 T2, Gamma |-- T1 === T2 -> True) /\    
+
+    (forall Gamma t1 t2 T, Gamma |-- t1 === t2 : T -> True) /\    
+
+    (forall Gamma sb1 sb2 Delta, Gamma |-- [sb1] === [sb2] : Delta ->  True)
+.
+Proof.
+eapply System_ind; intros; auto; subst.
+(* TP: TmNat *)
+assert (Delta |-- [SB] : Gamma) by (eapply RelSb_wellformed; eauto).
+destruct HDT; try solve [clear_inversion H1].
+simpl.
+eauto.
+(* TP: TmUnit *)
+assert (Delta |-- [SB] : Gamma) by (eapply RelSb_wellformed; eauto).
+destruct HDT; try solve [clear_inversion H1].
+simpl.
+eauto.
+(* TP: TmFun *)
+
+eapply Rel_Fundamental_Fun; eauto.
+
+ 
+(* TP: TmSb *)
+assert (Delta0 |-- [SB] : Gamma) as HX1 by (eapply RelSb_wellformed; eauto).
+
+clear_inversion H2.
+renamer.
+
+eapply RelType_ClosedForConversion.
+eauto.
+eapply EQ_TP_SYM.
+eapply EQ_TP_SBSEQ.
+eauto.
+eauto.
+eauto.
+
+(* TP: TmEmpty *)
+
+assert (Delta |-- [SB] : Gamma) by (eapply RelSb_wellformed; eauto).
+destruct HDT; try solve [clear_inversion H1].
+simpl.
+eauto.
+
+(* TmVar *)
+
+eapply Rel_Fundamental_Var; eauto.
+
+(* TmApp *)
+
+eapply Rel_Fundamental_App; eauto.
+
+(* TmAbs *)
+
+eapply Rel_Fundamental_Abs; eauto.
+
+(* Tm0 *)
+
+assert (Delta |-- [SB] : Gamma) by (eapply RelSb_wellformed; eauto).
+destruct HDT; try solve [clear_inversion H1].
+simpl.
+clear_inversion H2.
+repeat (split; auto).
+eauto.
+
+intros.
+exists Tm0.
+simpl.
+repeat (split; auto).
+apply reifyNf_n.
+ 
+
+eapply EQ_TRANS.
+eapply EQ_CONV.
+eapply EQ_CONG_SB.
+eauto.
+eapply EQ_SBNAT0.
+eauto.
+eauto.
+eapply EQ_SBNAT0.
+eauto.
+
+(* TmS *)
+
+eapply Rel_Fundamental_S; eauto.
+
+(* TmSb *)
+
+assert (Delta0 |-- [SB] : Gamma) as HX1 by (eapply RelSb_wellformed; eauto).
+
+clear_inversion H2.
+clear_inversion H3.
+compute_sth.
+renamer.
+
+assert (Delta0 |-- TmSb (TmSb A S) SB === TmSb A (Sseq S SB)) as HX2.
+eapply EQ_TP_SBSEQ.
+eauto.
+eauto.
+eauto.
+
+compute_sth. renamer.
+
+eapply RelTerm_ClosedForConversion.
+eauto.
+eauto.
+eauto.
+
+eapply EQ_SYM.
+eapply EQ_CONV.
+eapply EQ_SBSEQ.
+eauto.
+eauto.
+eauto.
+eauto.
+
+(* Tm1 *)
+assert (Delta |-- [SB] : Gamma) by (eapply RelSb_wellformed; eauto).
+destruct HDT; try solve [clear_inversion H1].
+simpl.
+repeat (split; auto).
+eauto.
+
+intros.
+exists Tm1.
+split; auto.
+unfold Ddown; simpl.
+auto.
+
+eapply EQ_Unit_Eta.
+eapply CONV.
+eapply Syntax.System.SB.
+eauto.
+eapply Syntax.System.SB.
+eauto.
+eauto.
+
+eapply EQ_TP_TRANS.
+eapply EQ_TP_CONG_SB.
+eauto.
+eapply EQ_TP_SB_UNIT.
+eauto.
+eapply EQ_TP_SB_UNIT.
+eauto.
+
+(* CONV *)
+
+assert ([denv] === [denv] #in# Gamma) as Hvalenv.
+eapply RelSb_valenv.
+eauto.
+
+assert (Gamma |= A === B) as Hvaleq.
+apply Valid_for_WfTpEq; auto.
+
+assert (Gamma |= t : A) as HvaltpA.
+apply Valid_for_WtTm; auto.
+
+assert (Delta |-- [SB]: Gamma) as HSB.
+eapply RelSb_wellformed.
+eauto.
+ 
+clear_inversion Hvaleq.
+specialize (H5 _ _ Hvalenv).
+
+destruct H5 as [DA [DB [HDA [HDB HDT']]]].
+compute_sth.
+renamer.
+
+clear_inversion HvaltpA.
+specialize (H6 _ _ Hvalenv).
+destruct H6 as [dtm0 [dtm1 [Hv1 [Hv2 [Hv3 [Hv4 Hv5]]]]]].
+destruct Hv2 as [PT [HPT1 HPT2]].
+compute_sth.
+renamer.
+
+specialize (H _ _ _ H1).
+specialize (H _ _ HDT').
+specialize (H _ HDA H3).
+
+assert (Delta ||- TmSb t SB : TmSb A SB #aeq# Dt_denv #in# HDT) as Hstep1.
+eapply RelTerm_ClosedUnderPer.
+eauto.
+eauto.
+eauto.
+
+eapply RelTerm_ClosedForConversion.
+eauto.
+eauto.
+eauto.
+eapply EQ_REFL.
+eauto.
+
+(* TmAbsurd *)
+
+eapply Rel_Fundamental_Absurd; eauto.
+
+(* SB: Sid *)
+clear_inversion H1.
+eapply RelSb_ClosedUnderEq.
+eapply EQ_SB_SYM.
+eapply EQ_SB_SIDL.
+eapply RelSb_wellformed.
+eauto.
+auto.
+
+(* SB: Sup *)
+
+clear_inversion H1.
+
+eapply RelSb_lift1_left.
+eauto.
+eauto.
+
+(* SB: Sseq *)
+
+clear_inversion H2.
+renamer.
+
+specialize (H _ _ _ H1 _ H5).
+specialize (H0 _ _ _ H _ H8).
+
+eapply RelSb_ClosedUnderEq.
+eapply EQ_SB_SYM.
+eapply EQ_SB_COMM.
+eapply RelSb_wellformed.
+eauto.
+eauto.
+eauto.
+eauto.
+ 
+(* SB: Sext *)
+
+clear_inversion H3.
+renamer.
+
+assert (Delta |= A) as HvalA.
+eapply Valid_for_WfTp; auto.
+
+assert (Gamma |= [S] : Delta) as HvalS.
+eapply Valid_for_WtSb; auto.
+
+assert ([denv] === [denv] #in# Gamma) as Hvalenv.
+eapply RelSb_valenv; eauto.
+
+clear_inversion HvalS.
+specialize (H5 _ _ Hvalenv).
+destruct H5 as [denv0 [denv1 [HX1 [HX2 HX3]]]].
+compute_sth.
+renamer.
+
+clear_inversion HvalA.
+specialize (H7 _ _ HX3).
+
+destruct H7 as [DA [DB [HDA1 [HDA2 HDA3]]]].
+compute_sth.
+renamer.
+
+eapply RelSb_ClosedUnderEq.
+eapply EQ_SB_SYM.
+eapply EQ_SB_SEXT.
+eapply RelSb_wellformed.
+eauto.
+eauto.
+
+
+specialize (H _ _ _ H2).
+specialize (H _ H6).
+
+
+assert (EvalTm (TmSb A S) denv DA_DS_denv) as HX4.
+eauto.
+
+specialize (H1 _ _ _ H2).
+specialize (H1 _ _ HDA3 _ HX4 H9).
+
+assert (Delta0 |-- [SB] : Gamma) as HY1 by (eapply RelSb_wellformed; eauto).
+
+assert (Delta0 ||- TmSb M SB : TmSb A (Sseq S SB) #aeq# DM_denv #in# HDA3) as HX5.
+eapply RelTerm_ClosedForConversion.
+eauto.
+eapply EQ_TP_SBSEQ.
+eauto.
+eauto.
+eauto.
+eauto.
+eapply EQ_REFL.
+eapply CONV.
+eapply Syntax.System.SB.
+eauto.
+eauto.
+eapply EQ_TP_REFL.
+eapply SB_F.
+eauto.
+eauto.
+
+
+specialize (H0 _ _ _ H).
+specialize (H0 DA_DS_denv DA_DS_denv HDA3 HDA1).
+
+
+assert (Gamma |= M : TmSb A S) as HvalTm.
+eapply Valid_for_WtTm; auto.
+clear_inversion HvalTm.
+specialize (H7 _ _ Hvalenv).
+destruct H7 as [dtm0 [dtm1 [PA [HD2 [HD3 [HD4 HD5]]]]]].
+compute_sth. renamer.
+auto.
+destruct HD2 as [d [HD2' HD2'']].
+
+econstructor 2 with (PX := PA).
+eauto.
+eapply H0.
+eauto.
+eapply EQ_SB_REFL.
+eapply SEXT.
+eapply SSEQ.
+eauto.
+eauto.
+eauto.
+
+eauto.
+ 
+(**)
+auto.
+auto.
+
+clear_inversion HD2'.
+auto. renamer.
+compute_sth.
+
+auto.
+Qed.
+
+ 
+(******************************************************************************
+ * Fundamental theorem for logical relations (unpack)
+ *)
+
+Theorem Rel_Fundamental_Tp: 
+    (forall Gamma T Delta SB denv DT (HDT : DT === DT #in# PerType),
+      Gamma |-- T ->
+      Delta ||- [SB] : Gamma #aeq# denv -> 
+          EvalTm T denv DT ->
+          Delta ||- TmSb T SB #in# HDT
+    ).
+Proof.
+intros.
+edestruct Rel_Fundamental; eauto.
+program_simpl.
+eauto.
+Qed.
+
+Theorem Rel_Fundamental_Tm:
+    (forall Gamma t T Delta SB denv DT (HDT : DT === DT #in# PerType) dt,
+      Gamma |-- t : T -> 
+      Delta ||- [SB] : Gamma #aeq# denv -> 
+          EvalTm T denv DT ->
+          EvalTm t denv dt ->
+          Delta ||- TmSb t SB : TmSb T SB #aeq# dt #in# HDT
+    ).
+
+Proof.
+intros.
+edestruct Rel_Fundamental; eauto.
+program_simpl.
+eauto.
+Qed.
+

Nbe/Model/LogRelSb/Fundamental_Helpers.v

+
+(******************************************************************************
+ * Pawel Wieczorek
+ *)
+
+Set Implicit Arguments.
+
+(*
+Add Rec LoadPath "../../Nbe" as Nbe.
+ *)
+
+
+Require Import Arith.
+Require Import Arith.Plus.
+
+Require Import Program.
+Require Import Program.Tactics.
+Require Import Program.Equality.
+Require Import Setoid.
+Require Import Relations.Relation_Definitions.
+Require Import Classes.RelationClasses.
+Add Rec LoadPath "../../Nbe" as Nbe.
+
+
+Require Import Nbe.Syntax.
+Require Import Nbe.Domain.
+Require Import Nbe.Utils.
+Require Import Nbe.Model.PER.
+Require Import Nbe.Model.Interp.
+Require Import Nbe.Model.Valid.
+Require Import Nbe.Model.Terminating.
+Require Import Nbe.Model.LogRelTm.
+Require Import Nbe.Model.LogRelSb.Def.
+Require Import Nbe.Model.LogRelSb.BasicFacts.
+
+
+(******************************************************************************
+ * Fundamental Theorem
+ *)
+
+
+Lemma Rel_Fundamental_Var: forall Delta Gamma T SB denv dt DT DT' (HDT : DT === DT' #in# PerType),
+  Gamma,,T |-- ->
+  Delta ||-  [SB]:Gamma,, T #aeq# denv ->
+  EvalTm (TmSb T Sup) denv DT ->
+  EvalTm TmVar denv dt ->
+  Delta ||- TmSb TmVar SB : TmSb (TmSb T Sup) SB #aeq# dt #in# HDT
+.
+Proof.
+intros.
+
+clear_inversion H0.
+
+clear_inversion H1.
+clear_inversion H2.
+clear_inversion H4.
+
+renamer.
+assert (DT_envs0 = DT_envs) as HY1.
+eauto.
+
+generalize dependent HDT.
+rewrite HY1 in *.
+clear HY1.
+clear DT_envs0.
+intros.
+compute_sth.
+
+assert (Delta |-- [sb] : Gamma) as HX1 by (eapply RelSb_wellformed; eauto).
+
+assert (Delta |-- [SB] : Gamma,,T) as HX2 by eauto.
+
+assert (Gamma |-- T) as HX3.
+assert (Gamma,,T |--) as HY1 by eauto.
+clear_inversion HY1; auto.
+
+assert (Delta |-- M : TmSb T sb) as HX4.
+eapply RelTerm_implies_WtTm.
+eauto.
+
+assert (Delta |-- TmSb (TmSb T Sup) SB === TmSb (TmSb T Sup) (Sext sb M)) as HX5.
+eapply EQ_TP_CONG_SB.
+eauto.
+eauto.
+
+assert (Delta |-- TmSb (TmSb T Sup) SB === TmSb T (Sseq Sup (Sext sb M))) as HX6.
+eapply EQ_TP_TRANS.
+eapply HX5.
+eapply EQ_TP_SBSEQ.
+eauto.
+eauto.
+eauto.
+
+
+
+assert (Delta |-- TmSb (TmSb T Sup) SB === TmSb T sb) as HX7.
+eapply EQ_TP_TRANS.
+eapply HX6.
+eapply EQ_TP_CONG_SB.
+eapply EQ_SB_SUP.
+eauto.
+eauto.
+eauto.
+eauto.
+
+assert (Delta |-- TmSb TmVar SB === M : TmSb (TmSb T Sup) SB) as HX8.
+eapply EQ_TRANS.
+eapply EQ_CONG_SB.
+eauto.
+eauto.
+eapply EQ_CONV.
+eapply EQ_SBVAR.
+eauto.
+eauto.
+eauto.
+eapply EQ_TP_SYM.
+eapply HX7.
+
+
+compute_sth; renamer.
+
+
+assert (Delta ||- M : TmSb T sb #aeq# dt #in# HDT) as HX9.
+eapply RelTerm_ClosedUnderPer_right; eauto.
+
+
+apply RelTerm_ClosedForConversion with (T := TmSb T sb) (t := M).
+eapply RelTerm_implies_RelType.
+eauto.
+
+eauto.
+eauto.
+eauto.
+Qed.
+
+Lemma Ssing_eq: forall SB B N A Gamma Delta,
+  Gamma |-- [SB] : Delta ->
+  Delta |-- N : A ->
+  Delta,,A |-- B ->
+  Gamma |-- TmSb (TmSb B (Ssing N)) SB === TmSb B (Sext SB (TmSb N SB))
+.
+Proof.
+intros.
+assert (Delta |-- A) as HX1.
+eauto.
+
+assert (Delta |-- N : TmSb A Sid) as HX2.
+eapply CONV.
+eauto.
+eauto.
+eauto.
+
+assert (Delta |--  [Sext Sid N] : Delta,,A) as HX3.
+eapply SEXT.
+eauto.
+eauto.
+eauto.
+
+
+unfold Ssing.
+eapply EQ_TP_TRANS.
+eapply EQ_TP_SBSEQ.
+eauto.
+eauto.
+eauto.
+
+eapply EQ_TP_CONG_SB.
+eapply EQ_SB_TRANS.
+eapply EQ_SB_SEXT.
+eauto.
+eauto.
+
+eapply EQ_SB_CONG_SEXT.
+eauto.
+eauto.
+eapply EQ_REFL.
+eapply CONV.
+eauto.
+eauto.
+eauto.
+Qed.
+
+
+
+
+Lemma Helper_Eq: forall Gamma A XA DA (HDA : DA === DA #in# PerType), 
+  Gamma ||- A #in# HDA ->
+  Gamma ||- XA #in# HDA ->
+  Gamma |-- A === XA.
+Proof.
+intros.
+edestruct RelType_Reify with (Gamma := Gamma) (T := A) (DT := DA) (HDT := HDA) as [Anf].
+auto.
+clear_inversion H1.
+
+edestruct RelType_Reify with (Gamma := Gamma) (T := XA) (DT := DA) (HDT := HDA) as [XAnf].
+eauto.
+clear_inversion H1.
+
+assert (Anf = XAnf).
+eapply RbNf_deter.
+eauto.
+eauto.
+subst.
+
+eapply EQ_TP_TRANS.
+eauto.
+auto.
+Qed.
+
+Lemma Helper_Eq' : forall Gamma A XA DA (HDA HDA' : DA === DA #in# PerType),
+  Gamma ||- A #in# HDA ->
+  Gamma ||- XA #in# HDA' ->
+  Gamma |-- A === XA.
+Proof.
+intros.
+
+assert (Gamma ||-  XA #in# HDA).
+eapply RelType_ProofIrrelevance.
+eauto.
+
+eapply Helper_Eq.
+eauto.
+eauto.
+Qed.
+
+Lemma Helper_Eq'' : forall Gamma A XA DA DA' (HDA : DA === DA' #in# PerType),
+  Gamma ||- A #in# HDA ->
+  Gamma ||- XA #in# HDA ->
+  Gamma |-- A === XA
+.
+Proof.
+intros.
+
+assert (DA === DA #in# PerType) as HDA_refl.
+eauto.
+
+assert (DA' === DA #in# PerType) as HDA_sym.
+symmetry.
+auto.
+
+assert (Gamma ||- A #in# HDA_sym) as HXX1.
+eapply RelType_ClosedUnderPer_sym.
+eauto.
+
+assert (Gamma ||- XA #in# HDA_sym) as HXX2.
+eapply RelType_ClosedUnderPer_sym.
+eauto.
+
+assert (Gamma ||- A #in# HDA_refl) as HXX3.
+eapply RelType_ClosedUnderPer.
+eauto.
+
+assert (Gamma ||- XA #in# HDA_refl) as HXX4.
+eapply RelType_ClosedUnderPer.
+eauto.
+
+eapply Helper_Eq.
+eauto.
+eauto.
+Qed.
+
+
+Lemma Rel_Fundamental_App: forall Gamma Delta M N SB A B dt DT DT' (HDT : DT === DT' #in# PerType) denv,
+  (forall (Delta : Cxt) (SB : Sb) (denv : DEnv),
+      Delta ||-  [SB]:Gamma #aeq# denv ->
+      forall (DT DT' : D) (HDT : DT === DT' #in# PerType) (dt : D),
+      EvalTm (TmFun A B) denv DT ->
+      EvalTm M denv dt ->
+      Delta ||- TmSb M SB : TmSb (TmFun A B) SB #aeq# dt #in# HDT
+  ) ->
+  (forall (Delta : Cxt) (SB : Sb) (denv : DEnv),
+       Delta ||-  [SB]:Gamma #aeq# denv ->
+       forall (DT DT' : D) (HDT : DT === DT' #in# PerType) (dt : D),
+       EvalTm A denv DT ->
+       EvalTm N denv dt -> Delta ||- TmSb N SB : TmSb A SB #aeq# dt #in# HDT
+  ) ->
+  ( forall (Delta : Cxt) (SB : Sb) (denv : DEnv),
+       Delta ||-  [SB]:Gamma,, A #aeq# denv ->
+       forall (DT DT' : D) (HDT : DT === DT' #in# PerType),
+       EvalTm B denv DT -> Delta ||- TmSb B SB #in# HDT
+  ) ->
+  Gamma |-- M : TmFun A B ->
+  Gamma |-- N : A ->
+  EvalTm (TmSb B (Ssing N)) denv DT ->
+  EvalTm (TmApp M N) denv dt ->
+  Delta ||-  [SB]:Gamma #aeq# denv ->
+   Delta ||- TmSb (TmApp M N) SB : TmSb (TmSb B (Ssing N)) SB #aeq# dt
+   #in# HDT
+.
+Proof.
+
+do 14 intro.
+intro Hnew.
+intros.
+ 
+clear_inversion H3.
+clear_inversion H4.
+clear_inversion H8.
+clear_inversion H6.
+compute_sth; renamer.
+
+specialize (H _ _ _ H5).
+specialize (H0 _ _ _ H5).
+
+assert ([envs0] === [envs0] #in# Gamma) as HX1.
+eapply RelSb_valenv.
+eauto.
+
+assert (Gamma |= M : TmFun A B) as HX2.
+apply Valid_for_WtTm; auto.
+
+clear_inversion HX2.
+
+specialize (H4 _ _ HX1).
+destruct H4 as [dtm0 [dtm1 [PF [H4' [H4'' [H4''' H4'''']]]]]].
+destruct H4' as [df [HY1 HY2]].
+clear_inversion HY1.
+compute_sth; renamer.
+(* checkpoit A *)
+
+clear_inversion H3.
+specialize (H6 _ _ HX1).
+destruct H6 as [DF [DF' [HZ1 [HZ2 HZ3]]]].
+(* checkpoint B *)
+
+elim_deters.
+clear HZ2.
+
+specialize (H _ _ HZ3).
+specialize (H DM_envs0).
+specialize (H HZ1 H7).
+
+assert (Gamma |= N : A) as HX3.
+apply Valid_for_WtTm; auto.
+clear_inversion HX3.
+(* checkpoint C *)
+
+specialize (H6 _ _ HX1).
+destruct H6 as [dn0 [dn1 [PA [H6' [H6'' [H6''' H6'''']]]]]].
+
+clear_inversion H3.
+specialize (H15 _ _ HX1).
+destruct H15 as [DA_ [DB_ [H15' [H15'' H15''']]]].
+(* checkpoint D *)
+
+elim_deters; clear_dups.
+
+clear_inversion HZ1.
+
+assert (DA = DA_envs0) as HQ1 by eauto.
+subst. clear_dups.
+
+(* checkpoint E *)
+
+clear_inversion H6'.
+clear_inversion H3.
+elim_deters; clear_dups.
+
+specialize (H0 _ _ H15''').
+specialize (H0 _ H12 H9).
+
+rename H0 into HREL_N.
+rename H into HREL_M.
+rename H15''' into HDA.
+rename HZ3 into HDF.
+
+assert (Delta |-- TmSb (TmFun A B) SB === TmFun (TmSb A SB) (TmSb B (Sext (Sseq SB Sup) TmVar))) as HX4.
+eapply EQ_TP_SB_FUN.
+eapply RelSb_wellformed.
+eauto.
+eauto.
+assert (Gamma |-- TmFun A B) as HY1.
+eauto.
+clear_inversion HY1.
+eauto.
+
+(* checkpoint F *)
+
+assert (Delta ||- TmSb M SB : TmFun (TmSb A SB) (TmSb B (Sext (Sseq SB Sup) TmVar))  #aeq# DM_envs0 #in# HDF) as HX5.
+eapply RelTerm_ClosedForConversion.
+eauto.
+eauto.
+eauto.
+eapply EQ_REFL.
+eapply RelTerm_implies_WtTm.
+eauto.
+
+(* pushing sb down *)
+
+assert (Delta |-- [SB] : Gamma) as HX7.
+eapply RelSb_wellformed.
+eauto.
+
+assert (Delta |-- TmSb (TmApp M N) SB === TmApp (TmSb M SB) (TmSb N SB) : TmSb (TmSb B (Ssing N)) SB) as HX6.
+eapply EQ_CONV.
+eapply EQ_SBAPP.
+eauto.
+eauto.
+eauto.
+eapply EQ_TP_SYM.
+eapply Ssing_eq; auto.
+eauto.
+eauto.
+assert (Gamma |-- TmFun A B) as HY1.
+eauto.
+clear_inversion HY1.
+eauto.
+
+cut (Delta ||- TmApp (TmSb M SB) (TmSb N SB) : TmSb (TmSb B (Ssing N)) SB #aeq# dt #in# HDT).
+intro.
+
+eapply RelTerm_ClosedForConversion.
+eauto.
+eauto.
+eauto.
+auto.
+
+(***)
+auto.
+
+generalize dependent HDF.
+generalize (eq_refl (Dfun DA_envs0 (Dclo B envs0))).
+generalize (eq_refl (Dfun DA_envs0 (Dclo B envs0))).
+
+generalize (Dfun DA_envs0 (Dclo B envs0)) at 1 5 7 9 as DF.
+generalize (Dfun DA_envs0 (Dclo B envs0)) at 2 4 5 6 as DF'.
+
+intros.
+
+(**) 
+ 
+induction HDF using PerType_dind; intros;
+try solve [clear_inversion H].
+clear_inversion H.
+clear_inversion H0.
+clear IHHDF.
+clear H3.
+simpl in HX5.
+
+destruct HX5 as [HC1 [XA [XF [PT [HC2 [HC3 [HC4 [HC5] ] ] ] ] ] ] ].
+
+specialize (H Delta 0).
+specialize (H (TmSb N SB)).
+specialize (H DN_envs0).
+
+destruct (e DN_envs0) as [DB HDB].
+find_extdeters.
+apply H0.
+apply H6''''.
+
+specialize (H DB DB).
+specialize (H PA H15 H6'''').
+specialize (H HDB HDB).
+
+assert (CxtShift Delta 0 Delta) as HCxt by eauto.
+specialize (H HCxt).
+
+(**)
+
+rename i into HDA'.
+rename i1 into HDT'.
+
+(**)
+
+(*** CRAZY ***)
+
+assert (Delta |-- TmSb A SB === XA) as HXX1.
+eapply Helper_Eq'.
+eauto.
+eauto.
+
+(**)
+
+move HREL_N at bottom.
+
+assert (Delta ||- TmSb N SB : TmSb A SB #aeq# DN_envs0 #in# HDA') as HXX2.
+eapply RelTerm_ProofIrrelevance; eauto.
+
+assert (Delta ||- TmSb N SB : TmSb XA (Sups 0) #aeq# DN_envs0 #in# HDA') as HXX3.
+eapply RelTerm_ClosedForConversion with (T := TmSb A SB) (T' := TmSb XA (Sups 0)).
+eauto.
+eapply EQ_TP_TRANS.
+apply HXX1.
+unfold Sups.
+apply EQ_TP_SYM.
+eapply EQ_TP_SBID.
+eauto.
+eauto.
+eapply EQ_REFL.
+eauto.
+
+(* ! *)
+
+specialize (H HXX3).
+
+destruct H as [dy].
+destruct H as [HYY1].
+unfold Sups in H.
+
+(**)
+
+generalize dependent DB.
+do 2 intro.
+inversion HDB.
+subst.
+assert (DB = DB_envs0_DN_envs0) as HXX4.
+eauto.
+subst.
+clear_dups.
+intros.
+
+(**)
+
+assert (dy = dt) as HXX4.
+eapply App_deter.
+eauto.
+eauto.
+subst.
+clear_dups.
+
+(**)
+
+assert (Delta ||- TmApp (TmSb (TmSb M SB) Sid) (TmSb N SB) : TmSb XF (Sext Sid (TmSb N SB)) #aeq# dt #in# HDT) as HXX4.
+eapply RelTerm_ClosedUnderPer''.
+eauto.
+
+(* new ---------------------------------*)
+
+assert (Delta |-- [Sext SB (TmSb N SB)] : Gamma,,A ) as HXX5.
+eapply SEXT.
+eauto.
+eauto.
+eauto.
+
+assert (Delta ||- [Sext SB (TmSb N SB)] : Gamma,,A #aeq# (Dext envs0 DN_envs0)) as HXX6.
+econstructor 2.
+eauto.
+eauto.
+eauto.
+eapply EQ_SB_REFL.
+eauto.
+eauto.
+eauto.
+eauto.
+eauto.
+
+
+move Hnew at bottom.
+specialize (Hnew _ _ _ HXX6).
+specialize (Hnew _ _ HDT H11).
+
+assert (Delta ||- TmSb XF (Sext Sid (TmSb N SB)) #in# HDT) as HXX7.
+eapply RelTerm_implies_RelType.
+eauto.
+
+assert (Delta |-- TmSb B (Sext SB (TmSb N SB)) === TmSb XF (Sext Sid (TmSb N SB))) as HXX8.
+eapply Helper_Eq''.
+eauto.
+eauto.
+
+assert (Gamma,,A |-- B) as HXX9.
+assert (Gamma |-- TmFun A B) as HYY1 by eauto.
+clear_inversion HYY1.
+auto.
+
+eapply RelTerm_ClosedForConversion.
+eauto.
+eapply EQ_TP_TRANS.
+eapply EQ_TP_SYM.
+eapply HXX8.
+
+eapply EQ_TP_SYM.
+eapply EQ_TP_TRANS.
+eapply EQ_TP_SBSEQ.
+eauto.
+unfold Ssing.
+eapply SEXT.
+eauto.
+eauto.
+eauto.
+eauto.
+
+eapply EQ_TP_CONG_SB.
+unfold Ssing.
+
+eapply EQ_SB_TRANS.
+eapply EQ_SB_SEXT.
+eauto.
+eapply SEXT.
+eauto.
+eauto.
+eauto.
+
+eapply EQ_SB_TRANS.
+eapply EQ_SB_CONG_SEXT.
+eapply EQ_SB_SIDL.
+eauto.
+eauto.
+eapply EQ_REFL.
+eapply CONV.
+eauto.
+
+eapply EQ_TP_TRANS.
+eapply EQ_TP_SBSEQ.
+eauto.
+eauto.
+eauto.
+
+eapply EQ_TP_CONG_SB.
+eapply EQ_SB_TRANS.
+eapply EQ_SB_SIDR.
+eauto.
+eapply EQ_SB_SYM.
+eapply EQ_SB_SIDL.
+eauto.
+eapply EQ_TP_REFL.
+eauto.
+
+eapply EQ_SB_REFL.
+eauto.
+
+eapply EQ_TP_REFL.
+eauto.
+
+eauto.
+
+eapply EQ_CONG_FUN_E.
+eapply EQ_SBID.
+eauto.
+
+eapply EQ_REFL.
+eauto.
+Qed.
+
+
+Lemma Rel_Fundamental_Abs: forall Gamma Delta A B M SB dt DT DT' (HDT: DT === DT' #in# PerType) denv,
+  Gamma,, A |-- M : B ->
+  (forall (Delta : Cxt) (SB : Sb) (denv : DEnv),
+      Delta ||-  [SB]:Gamma #aeq# denv ->
+      forall (DT DT' : D) (HDT : DT === DT' #in# PerType),
+      EvalTm A denv DT -> Delta ||- TmSb A SB #in# HDT
+  ) ->
+  ( forall (Delta : Cxt) (SB : Sb) (denv : DEnv),
+      Delta ||-  [SB]:Gamma,, A #aeq# denv ->
+      forall (DT DT' : D) (HDT : DT === DT' #in# PerType) (dt : D),
+      EvalTm B denv DT ->
+      EvalTm M denv dt -> Delta ||- TmSb M SB : TmSb B SB #aeq# dt #in# HDT
+  ) ->
+  Delta ||-  [SB]:Gamma #aeq# denv ->
+  EvalTm (TmFun A B) denv DT ->
+  EvalTm (TmAbs A M) denv dt ->
+  Delta ||- TmSb (TmAbs A M) SB : TmSb (TmFun A B) SB #aeq# dt #in# HDT
+.
+Proof.
+
+intros.
+rename H0 into Hnew.
+rename H1 into H0.
+rename H2 into H1.
+rename H3 into H2.
+rename H4 into H3.
+
+(* destroying HDT *)
+
+move HDT at bottom.
+remember DT as DTorg in H2.
+
+
+
+(****)
+
+clear_inversion H2.
+clear_inversion H3.
+renamer.
+
+(**)
+
+assert (Gamma,,A |--) as HX1.
+eauto.
+
+(**)
+
+assert (Delta |-- [SB] : Gamma) as HX2.
+eapply RelSb_wellformed.
+eauto.
+
+(**)
+
+assert (Delta |-- TmSb A SB) as HX3.
+eapply SB_F.
+eauto.
+clear_inversion HX1.
+auto.
+
+(**)
+
+assert (Delta,, TmSb A SB  |-- [Sext (Sseq SB Sup) TmVar] : Gamma,,A ) as HX4.
+eapply SEXT.
+eapply SSEQ.
+eapply SUP.
+auto.
+auto.
+clear_inversion HX1.
+auto.
+
+eapply CONV.
+eapply HYP.
+apply EXT.
+eauto.
+auto.
+
+(* eq *)
+eapply EQ_TP_SBSEQ.
+eapply SUP.
+auto.
+apply HX2.
+clear_inversion HX1.
+auto.
+
+(**)
+
+assert (Delta |-- TmSb (TmFun A B) SB === TmFun (TmSb A SB) (TmSb B (Sext (Sseq SB Sup) TmVar))) as HX10.
+eapply EQ_TP_SB_FUN.
+eauto.
+clear_inversion HX1.
+auto.
+eauto.
+
+assert (Delta |-- TmSb (TmAbs A M) SB === TmAbs (TmSb A SB) (TmSb M (Sext (Sseq SB Sup) TmVar)) : TmFun (TmSb A SB) (TmSb B (Sext (Sseq SB Sup) TmVar))) as HX11.
+eapply EQ_SBABS.
+eauto.
+auto.
+
+(* NEW *****)
+
+dependent inversion HDT. subst.
+
+renamer.
+rename i into HDA.
+rename i0 into HPA.
+rename i1 into HAPPDB.
+rename e into Hclo1.
+rename e0 into Hclo2.
+
+
+assert (exists PT, Interp (Dfun DA_denv (Dclo B denv)) PT) as HX20.
+eauto.
+
+
+simpl.
+
+(**)
+
+split.
+eapply System.SB.
+eauto.
+eapply FUN_I.
+
+assert (Gamma ,, A |--) as HYY1.
+eauto.
+clear_inversion HYY1.
+auto.
+auto.
+
+(**)
+
+exists (TmSb A SB).
+exists (TmSb B (Sext (Sseq SB Sup) TmVar)).
+destruct HX20 as [PT HPT].
+exists PT.
+split.
+
+(**)
+
+auto.
+split.
+
+(**)
+
+clear_inversion HPT.
+constructor 1.
+intros.
+
+assert (Gamma,,A |= M : B) as HXX21.
+apply Valid_for_WtTm; auto.
+
+clear_inversion HXX21.
+
+assert ( [Dext denv a0] === [Dext denv a1] #in# Gamma,,A) as HYY1.
+econstructor 2.
+eapply RelSb_valenv.
+eauto.
+red.
+exists DA_denv.
+split.
+auto.
+eauto.
+auto.
+
+specialize (H7 _ _ HYY1).
+destruct H7 as [dtm0 [dtm1 [PB HYY2] ] ].
+exists dtm0. exists dtm1.
+
+destruct HYY2.
+destruct H10.
+destruct H11.
+
+
+clear_inversion H5.
+clear_inversion po_ro.
+
+destruct H7 as [DBa0 HDBa0].
+destruct HDBa0.
+renamer.
+
+assert (a0 === a0 #in# PDA_denv0) as HYY3.
+eauto.
+
+destruct ro_resp_ex with a0 as [Y].
+auto.
+
+exists Y.
+ 
+split.
+auto.
+
+(**)
+
+
+repeat (split; auto).
+
+assert (Interp DB_denv_a0 Y) as HYY4.
+eapply H6.
+eauto.
+eauto.
+auto.
+
+assert (PDB_denv_a0 =~= Y) as HYY5.
+eauto.
+apply HYY5.
+eauto.
+
+(**)
+
+split.
+auto.
+split.
+auto.
+(**)
+
+eauto. 
+
+(**)
+
+intros.
+renamer.
+
+assert (Gamma,,A |= M : B) as HYY1.
+apply Valid_for_WtTm; auto.
+
+clear_inversion HYY1.
+
+assert ( [Dext denv da] === [Dext denv da] #in# Gamma,,A) as HYY2.
+econstructor 2.
+eapply RelSb_valenv.
+eauto.
+red.
+exists DA_denv.
+split.
+auto.
+eauto.
+auto.
+
+specialize (H5 _ _ HYY2).
+destruct H5 as [dtm0 [dtm1 [PB [HiDB [Hdtm0 [Hdtm1 HdtmPA ] ] ] ] ] ].
+exists dtm0.
+
+split.
+eauto.
+
+
+assert (Delta ||- TmSb A SB #in# HDA) as HYY3.
+eauto.
+
+assert (Delta0 ||- [Sseq SB (Sups i)] : Gamma #aeq# denv) as HYY4.
+eapply RelSb_ClosedUnderLift.
+eauto.
+eauto.
+
+assert (Gamma |-- A) as HYY5.
+assert (Gamma,,A |-- ) by eauto.
+clear_inversion H5.
+auto.
+
+assert (Delta0 |-- TmSb (TmSb A SB) (Sups i) === TmSb A (Sseq SB (Sups i))) as HYY6.
+eapply EQ_TP_SBSEQ.
+eauto.
+eauto.
+eauto.
+
+assert (Delta0 ||- a : TmSb A (Sseq SB (Sups i)) #aeq# da #in# HDA) as HYY7.
+eapply RelTerm_ClosedForConversion.
+eauto.
+eauto.
+eauto.
+eapply EQ_REFL.
+eapply RelTerm_implies_WtTm.
+eauto.
+
+assert (Delta0 ||- [Sext (Sseq SB (Sups i)) a] : Gamma,,A #aeq# Dext denv da) as HYY8.
+econstructor 2.
+eauto.
+eauto.
+eauto.
+eapply EQ_SB_REFL.
+eapply SEXT.
+eapply SSEQ.
+eauto.
+eauto.
+eauto.
+eapply RelTerm_implies_WtTm.
+eauto.
+eapply RelSb_valenv.
+eauto.
+eauto.
+eauto.
+eauto.
+
+move H0 at bottom.
+specialize (H0 Delta0 (Sext (Sseq SB (Sups i)) a) (Dext denv da)).
+specialize (H0 HYY8).
+specialize (H0 _ _ (  HAPPDB da da DB DB' PDA_denv0 HPA0 Hda Happ Happ' )).
+specialize (H0 dtm0).
+
+assert (EvalTm B (Dext denv da) DB) as HYY9.
+inversion Happ.
+auto.
+
+specialize (H0 HYY9 Hdtm0).
+
+
+assert (Delta0 |-- TmSb (TmSb B (Sext (Sseq SB Sup) TmVar)) (Sext (Sups i) a) === TmSb B (Sext (Sseq SB (Sups i)) a)) as HYY10.
+eapply EQ_TP_TRANS.
+eapply EQ_TP_SBSEQ.
+eapply SEXT.
+eauto.
+eauto.
+eapply RelTerm_implies_WtTm.
+eauto.
+eapply SEXT.
+eapply SSEQ.
+eauto.
+eauto.
+eauto.
+eapply CONV.
+eapply HYP.
+eapply EXT.
+eauto.
+eapply RelType_implies_WfTp.
+eauto.
+eapply EQ_TP_SBSEQ.
+eauto.
+eauto.
+eauto.
+eauto.
+eapply EQ_TP_CONG_SB.
+
+eapply EQ_SB_TRANS.
+eapply EQ_SB_SEXT.
+eapply SEXT.
+eauto.
+eauto.
+eapply RelTerm_implies_WtTm.
+eauto.
+eapply SEXT.
+eapply SSEQ.
+eauto.
+eauto.
+eauto.
+eapply CONV.
+eapply HYP.
+eapply EXT.
+eauto.
+eapply RelType_implies_WfTp.
+eauto.
+eapply EQ_TP_SBSEQ.
+eauto.
+eauto.
+eauto.
+
+assert ( Delta0 |-- a : TmSb (TmSb A SB) (Sups i)) as HZZZ0.
+eapply RelTerm_implies_WtTm.
+eauto.
+
+assert (Delta0 |--  [Sext (Sups i) a]: Delta,,TmSb A SB) as HZZZ1.
+eapply SEXT.
+eauto.
+eauto.
+auto.
+
+
+
+assert (Delta0 |-- [Sseq (Sseq SB Sup) (Sext (Sups i) a)] === [Sseq SB (Sups i)] : Gamma ) as HZZ1.
+eapply EQ_SB_TRANS.
+eapply EQ_SB_COMM.
+eauto.
+eauto.
+eauto.
+eauto.
+
+(**)
+eapply EQ_SB_CONG_SEXT.
+apply HZZ1.
+eauto.
+(**)
+
+assert (Delta0 |-- TmSb TmVar (Sext (Sups i) a) === a
+   : TmSb A (Sseq (Sseq SB Sup) (Sext (Sups i) a))) as HZZZ2.
+
+eapply EQ_CONV.
+eapply EQ_SBVAR.
+eauto.
+eauto.
+eapply RelTerm_implies_WtTm.
+eauto.
+eapply EQ_TP_TRANS.
+eapply EQ_TP_SBSEQ.
+eauto.
+eauto.
+eauto.
+eapply EQ_TP_CONG_SB.
+eapply EQ_SB_SYM.
+apply HZZ1.
+eauto.
+eauto.
+eauto.
+
+assert (Delta0 |-- TmApp (TmSb (TmSb (TmAbs A M) SB) (Sups i)) a ===  TmSb M (Sext (Sseq SB (Sups i)) a) : TmSb (TmSb B (Sext (Sseq SB Sup) TmVar)) (Sext (Sups i) a)) as HYY11.
+
+assert ( Delta0 |-- a : TmSb (TmSb A SB) (Sups i)) as HZZZ0.
+eapply RelTerm_implies_WtTm.
+eauto.
+
+assert (Delta0 |--  [Sext (Sups i) a]: Delta,,TmSb A SB) as HZZZ1.
+eapply SEXT.
+eauto.
+eauto.
+auto.
+
+
+assert (Delta0 |-- a : TmSb (TmSb A (Sseq SB (Sups i))) Sid) as HZZ1.
+eapply CONV.
+eapply RelTerm_implies_WtTm.
+eauto.
+eapply EQ_TP_SYM.
+eapply EQ_TP_SBID.
+eapply RelType_implies_WfTp with (T := TmSb A (Sseq SB (Sups i)) ).
+eapply RelTerm_implies_RelType.
+eauto. 
+
+
+
+assert ( Delta0,, TmSb A (Sseq SB (Sups i)) |-- TmVar
+   : TmSb A (Sseq (Sseq SB (Sups i)) Sup)) as HZZ2.
+
+eapply CONV.
+eapply HYP.
+eapply EXT.
+eauto.
+eapply RelType_implies_WfTp with (T := TmSb A (Sseq SB (Sups i)) ).
+eapply RelTerm_implies_RelType.
+
+eauto.
+eapply EQ_TP_SBSEQ.
+eauto.
+eauto.
+eauto.
+
+assert (Delta0 |-- a : TmSb A (Sseq SB (Sups i))) as HZZ3.
+eapply RelTerm_implies_WtTm.
+eauto.
+
+
+
+assert (Delta0 |-- [Sseq (Sseq SB Sup) (Sext (Sups i) a)] === [Sseq SB (Sups i)] : Gamma ) as HZZ4.
+eapply EQ_SB_TRANS.
+eapply EQ_SB_COMM.
+eauto.
+eauto.
+eauto.
+eapply EQ_SB_CONG_SSEQ.
+eapply EQ_SB_SUP.
+eauto.
+eauto.
+eauto.
+eauto.
+
+assert (Delta0 |--  [Sext Sid a]: Delta0,, TmSb A (Sseq SB (Sups i))) as HZZZ4.
+eapply SEXT.
+eauto.
+eauto.
+auto.
+
+assert (Delta0 |--  [Sseq (Sseq (Sseq SB (Sups i)) Sup) (Sext Sid a)]===
+   [Sseq SB (Sups i)]:Gamma) as HZZ5.
+eapply EQ_SB_TRANS.
+eapply EQ_SB_COMM.
+eauto.
+eauto.
+eauto.
+
+eapply EQ_SB_TRANS.
+eapply EQ_SB_CONG_SSEQ.
+eapply EQ_SB_SUP.
+eauto.
+eapply RelType_implies_WfTp with (T := TmSb A (Sseq SB (Sups i)) ).
+eapply RelTerm_implies_RelType.
+eauto.
+auto.
+eapply EQ_SB_REFL.
+eauto.
+eapply EQ_SB_TRANS.
+eapply EQ_SB_SIDR.
+eauto.
+eapply EQ_SB_REFL.
+eauto.
+
+(*
+assert (Delta0 |-- TmSb TmVar (Sext (Sups i) a) === a
+   : TmSb A (Sseq (Sseq SB Sup) (Sext (Sups i) a))) as HZZZ2.
+
+eapply EQ_CONV.
+eapply EQ_SBVAR.
+eauto.
+eauto.
+eapply RelTerm_implies_WtTm.
+eauto.
+eapply EQ_TP_TRANS.
+eapply EQ_TP_SBSEQ.
+eauto.
+eauto.
+eauto.
+eapply EQ_TP_CONG_SB.
+eapply EQ_SB_SYM.
+apply HZZ1.
+eauto.
+eauto.
+*)
+
+
+
+assert (
+  Delta0
+   |-- TmSb B (Sseq (Sext (Sseq (Sseq SB (Sups i)) Sup) TmVar) (Sext Sid a)) ===
+   TmSb (TmSb B (Sext (Sseq (Sseq SB (Sups i)) Sup) TmVar)) (Sext Sid a)
+) as HZZ6.
+eapply EQ_TP_SYM.
+eapply EQ_TP_SBSEQ.
+eauto.