Commits

Paweł Wieczorek committed be5f7e7

Added WIP-file

Comments (0)

Files changed (5)

 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/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/LogRelSb_Fundamental.v

 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: 

Nbe/Model/LogRelSb_Fundamental_Helpers.v

  
 
 
-Theorem Rel_Fundamental_Absurd: forall Gamma A Delta SB denv DT DT' (HDT : DT === DT' #in# PerType) dt,
-  Gamma |-- A ->
-  (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) ->
-  Delta ||-  [SB]:Gamma #aeq# denv ->
-  EvalTm (TmArr TmEmpty A) denv DT ->
-  EvalTm (TmAbsurd A) denv dt ->
-  Delta ||- TmSb (TmAbsurd A) SB : TmSb (TmArr TmEmpty A) SB #aeq# dt
-   #in# HDT
-.
-Proof.
-intros.
-
-unfold TmArr in *.
-clear_inversion H2.
-clear_inversion H8.
-clear_inversion H3.
-
-dependent inversion HDT; subst.
-
-rename i into HDempty.
-rename i0 into HInterp.
-rename e into HappDF.
-rename e0 into HappDF'.
-rename i1 into HREC.
-
-inversion HInterp; subst.
-
-(**)
-
-assert (Delta |-- [SB] : Gamma) as HYY1.
-eapply RelSb_wellformed.
-eauto.
-
-simpl.
-split.
-
-eapply System.SB.
-eauto.
-eapply EMPTY_E.
-auto.
-
-exists TmEmpty. 
-exists (TmSb A (Sseq SB Sup)).
-
-assert (exists PT, Interp (Dfun Dempty (Dclo (TmSb A Sup) denv)) PT) as HYY2.
-eauto.
-
-destruct HYY2 as [PT HPT].
-exists PT.
-split; auto.
-
-clear_inversion HPT.
-clear_inversion H5.
-
-split.
-
-(**)
-
-constructor 1.
-intros. 
-inversion H2; subst.
-rename H2 into Hempty.
-rename H3 into H2.
-
-exists (Dup DA (DneAbsurd (DdownN DA) e)).
-exists (Dup DA (DneAbsurd (DdownN DA) e')).
-
-clear_inversion H6.
-clear_inversion po_ro.
-destruct ro_resp_ex with (Dup Dempty e) as [Y HY].
-eauto.
- 
-exists Y.
-split.
-eauto.
-
-split.
-unfold Dup at 1. simpl. 
-eauto.
-
-split.
-unfold Dup at 1. simpl. 
-eauto.
-
-assert (Gamma |= A).
-eapply Valid_for_WfTp.
-eauto.
-
-clear_inversion H3.
-assert ([denv] === [denv] #in# Gamma).
-eapply RelSb_valenv.
-eauto.
-
-specialize (H6 _ _ H3).
-destruct H6.
-destruct H6.
-destruct H6.
-destruct H8.
-renamer.
-elim_deters.
-
-eapply Reflect_Characterization.
-eauto.
-
-assert (Dup Dempty e === Dup Dempty e #in# PerEmpty) as He.
-eauto.
-
-eapply H7.
-
-eapply He.
-eauto.
-eauto.
-
-constructor 1.
-intros.
-
-
-clear_inversion H2.
-
-assert (exists PA, Interp DA_denv1 PA) as HPA.
-eauto.
-destruct HPA as [PA HPA].
-
-assert (DdownN DA_denv1 === DdownN DA_denv1 #in# PerNf) as Htp.
-eapply ReifyTp_Characterization.
-eauto.
-eauto.
-
-clear_inversion Htp.
-
-edestruct H10 as [ne [Hne Hne']].
-edestruct H2 as [NFA [HNFA _]].
-
-eexists.
-split.
-eauto.
-eauto.
-
-(**)
-
-
-assert (Delta,, TmSb TmEmpty SB |--  [Sext (Sseq SB Sup) TmVar]: Gamma,, TmEmpty) as HXX1.
-eapply SEXT.
-eapply SSEQ.
-eauto.
-eauto.
-eauto.
-eapply CONV.
-eapply HYP.
-eapply EXT.
-eauto.
-eapply SB_F.
-eauto.
-eauto.
-eapply EQ_TP_TRANS.
-eapply EQ_TP_SBSEQ.
-eauto.
-eauto.
-eauto.
-eapply EQ_TP_REFL.
-eapply SB_F.
-eauto.
-eauto.
-
-(**)
-split.
-
-eapply EQ_TP_TRANS.
-eapply EQ_TP_SB_FUN.
-eauto.
-eauto.
-eauto.
-
-eapply EQ_TP_CONG_FUN.
-eauto.
-
-eapply EQ_TP_TRANS.
-eapply EQ_TP_SBSEQ.
-eauto.
-eauto.
-eauto.
-
-eapply EQ_TP_CONG_SB.
-eapply EQ_SB_TRANS.
-eapply EQ_SB_SUP.
-eauto.
-eapply EMPTY_F.
-eauto.
-eapply CONV.
-eapply HYP.
-eauto.
-eapply EQ_TP_SBSEQ.
-eauto.
-eauto.
-eauto.
-eapply EQ_SB_REFL.
-eauto.
-eauto.
-
-eapply EQ_TP_TRANS.
-eapply EQ_TP_SBSEQ.
-eapply SEXT.
-eauto.
-eapply EMPTY_F.
-eauto.
-eapply CONV.
-eapply HYP.
-eapply EXT.
-eauto.
-eauto.
-
-eapply EQ_TP_TRANS.
-eapply EQ_TP_SB_EMPTY.
-eauto.
-eapply EQ_TP_SYM.
-eapply EQ_TP_SB_EMPTY.
-eauto.
-eauto.
-eauto.
-eapply EQ_TP_CONG_SB.
-
-eapply EQ_SB_TRANS.
-eapply EQ_SB_SUP.
-eauto.
-eapply EMPTY_F.
-eauto.
-
-eapply CONV.
-eapply HYP.
-eauto.
-eapply EXT.
-eauto.
-eauto.
-
-eapply EQ_TP_TRANS.
-eapply EQ_TP_SB_EMPTY.
-eauto.
-eapply EQ_TP_SYM.
-eapply EQ_TP_SB_EMPTY.
-eauto.
-eapply EQ_SB_REFL.
-eauto.
-eauto.
-
-(****)
-split.
-
-dependent inversion HDempty.
-subst; simpl.
-eauto.
-
-(*****)
-
-intros.
-inversion HPA; subst.
-inversion Hda; subst.
-
-eexists.
-split.
-unfold Dup; simpl; eauto.
-
-inversion Happ; subst.
-clear_inversion H13.
-clear_inversion H11.
-elim_deters.
-renamer.
-clear_dups.
-
-
-(**)
-
-assert ( Delta0 |-- [Sseq SB (Sups i)] : Gamma ) as HXX2.
-eauto.
-
-assert ( Delta0 ||- [Sseq SB (Sups i)] : Gamma #aeq# envs ) as HXX3.
-eapply RelSb_ClosedUnderLift.
-eauto.
-eauto.
-
-
-assert (Delta0 |-- a :  TmSb TmEmpty (Sups i)) as HXX4.
-eapply RelTerm_implies_WtTm.
-eauto.
-
-assert (Delta0 |-- a :  TmEmpty) as HXX5.
-eapply CONV.
-eauto.
-eapply EQ_TP_SB_EMPTY.
-eauto.
-
-assert (Delta0 |--  [Sext (Sups i) a]: Delta,,TmEmpty) as HXX7.
-eapply SEXT.
-eauto.
-eauto.
-eauto.
-
-
-assert (Delta0 |--  TmSb (TmSb A (Sseq SB Sup)) (Sext (Sups i) a) === TmSb A (Sseq SB (Sups i))) as HXX6.
-eapply EQ_TP_TRANS.
-eapply EQ_TP_SBSEQ.
-eauto.
-eauto.
-eauto.
-
-eapply EQ_TP_CONG_SB.
-eapply EQ_SB_TRANS.
-eapply EQ_SB_COMM.
-eauto.
-eauto.
-eauto.
-
-eapply EQ_SB_CONG_SSEQ.
-eapply EQ_SB_SUP.
-eauto.
-eapply EMPTY_F.
-eauto.
-eauto.
-eapply EQ_SB_REFL.
-eauto.
-eauto.
-
-(**)
-
-assert ( Delta0 ||- TmSb (TmSb A (Sseq SB Sup)) (Sext (Sups i) a)
-   #in# HREC (Dup Dempty e) (Dup Dempty e) DA_envs0 DB' PerEmpty HPA Hda Happ
-          Happ') as HZZ2.
-
-eapply RelType_ClosedForConversion.
-eauto.
-eauto.
-
-specialize (H0 _ _ _ HXX3).
-specialize (H0 _ _ (HREC (Dup Dempty e) (Dup Dempty e) DA_envs0 DB' PerEmpty HPA Hda Happ
-          Happ')).
-specialize (H0 H15).
- 
-edestruct RelReify1.
-eauto.
-destruct H8 as [RelTerm_Reify_ RelTerm_Back_ ].
-rename H4 into RelType_Reify_.
-eapply RelTerm_Back_.
-
-
-(****)
-renamer.
-assert (DdownN DA_envs === DdownN DA_envs #in# PerNf) as HXXX4.
-
-assert (Gamma |= A) as HXXX2.
-eapply Valid_for_WfTp.
-eauto.
-
-
-clear_inversion HXXX2.
-assert ([envs] === [envs] #in# Gamma) as HXXX3.
-eapply RelSb_valenv.
-eauto.
-
-specialize (H8 _ _ HXXX3).
-destruct H8 as [DA_ [ _DA [_HDA [HDA_ HDA]]]].
-
-elim_deters.
-renamer.
-
-assert (exists PT, Interp DA_envs PT) as HPT.
-eauto.
-
-destruct HPT as [PT HPT].
-renamer.
- 
-eapply ReifyTp_Characterization.
-eauto.
-eauto.
-clear_inversion HXXX4.
-
-(**)
-constructor 1.
-
-intros.
-
-clear_inversion H5.
-
-edestruct H8 as [ne [Hne1 Hne2]].
-edestruct H4 as [NFA [HNFA1 HNFA2]].
-eexists.
-split.
-eauto.
-eauto.
-
-(*****)
-
-intros.
-renamer.
-assert (DdownN DA_envs === DdownN DA_envs #in# PerNf) as HXXX4.
-
-assert (Gamma |= A) as HXXX2.
-eapply Valid_for_WfTp.
-eauto.
-
-
-clear_inversion HXXX2.
-assert ([envs] === [envs] #in# Gamma) as HXXX3.
-eapply RelSb_valenv.
-eauto.
-
-specialize (H10 _ _ HXXX3).
-destruct H10 as [DA_ [ _DA [_HDA [HDA_ HDA]]]].
-
-elim_deters.
-renamer.
-
-assert (exists PT, Interp DA_envs PT) as HPT.
-eauto.
-
-destruct HPT as [PT HPT].
-renamer.
- 
-eapply ReifyTp_Characterization.
-eauto.
-eauto.
-clear_inversion HXXX4.
-inversion H5; subst.
- 
-edestruct H10 as [ne [Hne1 Hne2]].
-edestruct H8 as [NFA [HNFA1 HNFA2]].
-eexists.
-split.
-eauto.
-
-(**)
-
-
-
-assert (Delta1 |-- TmSb (TmApp (TmSb (TmSb (TmAbsurd A) SB) (Sups i)) a) (Sups i0) === TmApp (TmAbsurd (TmSb A (Sseq SB (Sups (i + i0))))) (TmSb a (Sups i0)) : TmSb (TmSb (TmSb A (Sseq SB Sup)) (Sext (Sups i) a)) (Sups i0)) as HZZ3.
-
-eapply EQ_TRANS.
-eapply EQ_CONG_SB.
-eauto.
-eapply EQ_CONV.
-eapply EQ_CONG_FUN_E.
-eapply EQ_CONV.
-eapply EQ_SBSEQ.
-eauto.
-eauto.
-eauto.
-
-eapply EQ_TP_TRANS.
-eapply EQ_TP_SBSEQ.
-eauto.
-eauto.
-eauto.
-
-eapply EQ_TP_TRANS.
-eapply EQ_TP_SB_ARR.
-eauto.
-eauto.
-eauto.
-eapply EQ_TP_REFL.
-eapply FUN_F.
-eapply SB_F.
-eauto.
-eauto.
-
-eapply SB_F.
-eauto.
-eapply SB_F.
-eauto.
-eauto.
-eapply EQ_REFL.
-eauto.
-
-
-(*
-destruct RelType_Reify_ as [NFA' [HNFA1' HNFA''] ].
-renamer.
-*)
-
-admit.
-admit.
-admit.
-
-Qed.
-
-

Nbe/Model/LogRelSb_Fundamental_WIP.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.
+
+
+
+Theorem Rel_Fundamental_Absurd: forall Gamma A Delta SB denv DT DT' (HDT : DT === DT' #in# PerType) dt,
+  Gamma |-- A ->
+  (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) ->
+  Delta ||-  [SB]:Gamma #aeq# denv ->
+  EvalTm (TmArr TmEmpty A) denv DT ->
+  EvalTm (TmAbsurd A) denv dt ->
+  Delta ||- TmSb (TmAbsurd A) SB : TmSb (TmArr TmEmpty A) SB #aeq# dt
+   #in# HDT
+.
+Proof.
+intros.
+
+unfold TmArr in *.
+clear_inversion H2.
+clear_inversion H8.
+clear_inversion H3.
+
+dependent inversion HDT; subst.
+
+rename i into HDempty.
+rename i0 into HInterp.
+rename e into HappDF.
+rename e0 into HappDF'.
+rename i1 into HREC.
+
+inversion HInterp; subst.
+
+(**)
+
+assert (Delta |-- [SB] : Gamma) as HYY1.
+eapply RelSb_wellformed.
+eauto.
+
+simpl.
+split.
+
+eapply System.SB.
+eauto.
+eapply EMPTY_E.
+auto.
+
+exists TmEmpty. 
+exists (TmSb A (Sseq SB Sup)).
+
+assert (exists PT, Interp (Dfun Dempty (Dclo (TmSb A Sup) denv)) PT) as HYY2.
+eauto.
+
+destruct HYY2 as [PT HPT].
+exists PT.
+split; auto.
+
+clear_inversion HPT.
+clear_inversion H5.
+
+split.
+
+(**)
+
+constructor 1.
+intros. 
+inversion H2; subst.
+rename H2 into Hempty.
+rename H3 into H2.
+
+exists (Dup DA (DneAbsurd (DdownN DA) e)).
+exists (Dup DA (DneAbsurd (DdownN DA) e')).
+
+clear_inversion H6.
+clear_inversion po_ro.
+destruct ro_resp_ex with (Dup Dempty e) as [Y HY].
+eauto.
+ 
+exists Y.
+split.
+eauto.
+
+split.
+unfold Dup at 1. simpl. 
+eauto.
+
+split.
+unfold Dup at 1. simpl. 
+eauto.
+
+assert (Gamma |= A).
+eapply Valid_for_WfTp.
+eauto.
+
+clear_inversion H3.
+assert ([denv] === [denv] #in# Gamma).
+eapply RelSb_valenv.
+eauto.
+
+specialize (H6 _ _ H3).
+destruct H6.
+destruct H6.
+destruct H6.
+destruct H8.
+renamer.
+elim_deters.
+
+eapply Reflect_Characterization.
+eauto.
+
+assert (Dup Dempty e === Dup Dempty e #in# PerEmpty) as He.
+eauto.
+
+eapply H7.
+
+eapply He.
+eauto.
+eauto.
+
+constructor 1.
+intros.
+
+
+clear_inversion H2.
+
+assert (exists PA, Interp DA_denv1 PA) as HPA.
+eauto.
+destruct HPA as [PA HPA].
+
+assert (DdownN DA_denv1 === DdownN DA_denv1 #in# PerNf) as Htp.
+eapply ReifyTp_Characterization.
+eauto.
+eauto.
+
+clear_inversion Htp.
+
+edestruct H10 as [ne [Hne Hne']].
+edestruct H2 as [NFA [HNFA _]].
+
+eexists.
+split.
+eauto.
+eauto.
+
+(**)
+
+
+assert (Delta,, TmSb TmEmpty SB |--  [Sext (Sseq SB Sup) TmVar]: Gamma,, TmEmpty) as HXX1.
+eapply SEXT.
+eapply SSEQ.
+eauto.
+eauto.
+eauto.
+eapply CONV.
+eapply HYP.
+eapply EXT.
+eauto.
+eapply SB_F.
+eauto.
+eauto.
+eapply EQ_TP_TRANS.
+eapply EQ_TP_SBSEQ.
+eauto.
+eauto.
+eauto.
+eapply EQ_TP_REFL.
+eapply SB_F.
+eauto.
+eauto.
+
+(**)
+split.
+
+eapply EQ_TP_TRANS.
+eapply EQ_TP_SB_FUN.
+eauto.
+eauto.
+eauto.
+
+eapply EQ_TP_CONG_FUN.
+eauto.
+
+eapply EQ_TP_TRANS.
+eapply EQ_TP_SBSEQ.
+eauto.
+eauto.
+eauto.
+
+eapply EQ_TP_CONG_SB.
+eapply EQ_SB_TRANS.
+eapply EQ_SB_SUP.
+eauto.
+eapply EMPTY_F.
+eauto.
+eapply CONV.
+eapply HYP.
+eauto.
+eapply EQ_TP_SBSEQ.
+eauto.
+eauto.
+eauto.
+eapply EQ_SB_REFL.
+eauto.
+eauto.
+
+eapply EQ_TP_TRANS.
+eapply EQ_TP_SBSEQ.
+eapply SEXT.
+eauto.
+eapply EMPTY_F.
+eauto.
+eapply CONV.
+eapply HYP.
+eapply EXT.
+eauto.
+eauto.
+
+eapply EQ_TP_TRANS.
+eapply EQ_TP_SB_EMPTY.
+eauto.
+eapply EQ_TP_SYM.
+eapply EQ_TP_SB_EMPTY.
+eauto.
+eauto.
+eauto.
+eapply EQ_TP_CONG_SB.
+
+eapply EQ_SB_TRANS.
+eapply EQ_SB_SUP.
+eauto.
+eapply EMPTY_F.
+eauto.
+
+eapply CONV.
+eapply HYP.
+eauto.
+eapply EXT.
+eauto.
+eauto.
+
+eapply EQ_TP_TRANS.
+eapply EQ_TP_SB_EMPTY.
+eauto.
+eapply EQ_TP_SYM.
+eapply EQ_TP_SB_EMPTY.
+eauto.
+eapply EQ_SB_REFL.
+eauto.
+eauto.
+
+(****)
+split.
+
+dependent inversion HDempty.
+subst; simpl.
+eauto.
+
+(*****)
+
+intros.
+inversion HPA; subst.
+inversion Hda; subst.
+
+eexists.
+split.
+unfold Dup; simpl; eauto.
+
+inversion Happ; subst.
+clear_inversion H13.
+clear_inversion H11.
+elim_deters.
+renamer.
+clear_dups.
+
+
+(**)
+
+assert ( Delta0 |-- [Sseq SB (Sups i)] : Gamma ) as HXX2.
+eauto.
+
+assert ( Delta0 ||- [Sseq SB (Sups i)] : Gamma #aeq# envs ) as HXX3.
+eapply RelSb_ClosedUnderLift.
+eauto.
+eauto.
+
+
+assert (Delta0 |-- a :  TmSb TmEmpty (Sups i)) as HXX4.
+eapply RelTerm_implies_WtTm.
+eauto.
+
+assert (Delta0 |-- a :  TmEmpty) as HXX5.
+eapply CONV.
+eauto.
+eapply EQ_TP_SB_EMPTY.
+eauto.
+
+assert (Delta0 |--  [Sext (Sups i) a]: Delta,,TmEmpty) as HXX7.
+eapply SEXT.
+eauto.
+eauto.
+eauto.
+
+
+assert (Delta0 |--  TmSb (TmSb A (Sseq SB Sup)) (Sext (Sups i) a) === TmSb A (Sseq SB (Sups i))) as HXX6.
+eapply EQ_TP_TRANS.
+eapply EQ_TP_SBSEQ.
+eauto.
+eauto.
+eauto.
+
+eapply EQ_TP_CONG_SB.
+eapply EQ_SB_TRANS.
+eapply EQ_SB_COMM.
+eauto.
+eauto.
+eauto.
+
+eapply EQ_SB_CONG_SSEQ.
+eapply EQ_SB_SUP.
+eauto.
+eapply EMPTY_F.
+eauto.
+eauto.
+eapply EQ_SB_REFL.
+eauto.
+eauto.
+
+(**)
+
+assert ( Delta0 ||- TmSb (TmSb A (Sseq SB Sup)) (Sext (Sups i) a)
+   #in# HREC (Dup Dempty e) (Dup Dempty e) DA_envs0 DB' PerEmpty HPA Hda Happ
+          Happ') as HZZ2.
+
+eapply RelType_ClosedForConversion.
+eauto.
+eauto.
+
+specialize (H0 _ _ _ HXX3).
+specialize (H0 _ _ (HREC (Dup Dempty e) (Dup Dempty e) DA_envs0 DB' PerEmpty HPA Hda Happ
+          Happ')).
+specialize (H0 H15).
+ 
+edestruct RelReify1.
+eauto.
+destruct H8 as [RelTerm_Reify_ RelTerm_Back_ ].
+rename H4 into RelType_Reify_.
+eapply RelTerm_Back_.
+
+
+(****)
+renamer.
+assert (DdownN DA_envs === DdownN DA_envs #in# PerNf) as HXXX4.
+
+assert (Gamma |= A) as HXXX2.
+eapply Valid_for_WfTp.
+eauto.
+
+
+clear_inversion HXXX2.
+assert ([envs] === [envs] #in# Gamma) as HXXX3.
+eapply RelSb_valenv.
+eauto.
+
+specialize (H8 _ _ HXXX3).
+destruct H8 as [DA_ [ _DA [_HDA [HDA_ HDA]]]].
+
+elim_deters.
+renamer.
+
+assert (exists PT, Interp DA_envs PT) as HPT.
+eauto.
+
+destruct HPT as [PT HPT].
+renamer.
+ 
+eapply ReifyTp_Characterization.
+eauto.
+eauto.
+clear_inversion HXXX4.
+
+(**)
+constructor 1.
+
+intros.
+
+clear_inversion H5.
+
+edestruct H8 as [ne [Hne1 Hne2]].
+edestruct H4 as [NFA [HNFA1 HNFA2]].
+eexists.
+split.
+eauto.
+eauto.
+
+(*****)
+
+intros.
+renamer.
+assert (DdownN DA_envs === DdownN DA_envs #in# PerNf) as HXXX4.
+
+assert (Gamma |= A) as HXXX2.
+eapply Valid_for_WfTp.
+eauto.
+
+
+clear_inversion HXXX2.
+assert ([envs] === [envs] #in# Gamma) as HXXX3.
+eapply RelSb_valenv.
+eauto.
+
+specialize (H10 _ _ HXXX3).
+destruct H10 as [DA_ [ _DA [_HDA [HDA_ HDA]]]].
+
+elim_deters.
+renamer.
+
+assert (exists PT, Interp DA_envs PT) as HPT.
+eauto.
+
+destruct HPT as [PT HPT].
+renamer.
+ 
+eapply ReifyTp_Characterization.
+eauto.
+eauto.
+clear_inversion HXXX4.
+inversion H5; subst.
+ 
+edestruct H10 as [ne [Hne1 Hne2]].
+edestruct H8 as [NFA [HNFA1 HNFA2]].
+eexists.
+split.
+eauto.
+
+(**)
+
+
+
+assert (Delta1 |-- TmSb (TmApp (TmSb (TmSb (TmAbsurd A) SB) (Sups i)) a) (Sups i0) === TmApp (TmAbsurd (TmSb A (Sseq SB (Sups (i + i0))))) (TmSb a (Sups i0)) : TmSb (TmSb (TmSb A (Sseq SB Sup)) (Sext (Sups i) a)) (Sups i0)) as HZZ3.
+
+eapply EQ_TRANS.
+eapply EQ_CONG_SB.
+eauto.
+eapply EQ_CONV.
+eapply EQ_CONG_FUN_E.
+eapply EQ_CONV.
+eapply EQ_SBSEQ.
+eauto.
+eauto.
+eauto.
+
+eapply EQ_TP_TRANS.
+eapply EQ_TP_SBSEQ.
+eauto.
+eauto.
+eauto.
+
+eapply EQ_TP_TRANS.
+eapply EQ_TP_SB_ARR.
+eauto.
+eauto.
+eauto.
+eapply EQ_TP_REFL.
+eapply FUN_F.
+eapply SB_F.
+eauto.
+eauto.
+
+eapply SB_F.
+eauto.
+eapply SB_F.
+eauto.
+eauto.
+eapply EQ_REFL.
+eauto.
+
+
+(*
+destruct RelType_Reify_ as [NFA' [HNFA1' HNFA''] ].
+renamer.
+*)
+
+admit.
+admit.
+admit.
+
+Qed.
+
+