Commits

Paweł Wieczorek committed 32cf3ea

Splitting LogRelSb into smaller files

Comments (0)

Files changed (9)

 Nbe/Model/LogRelTm_ClosedUnderPer.v
 Nbe/Model/LogRelTm_Lift.v
 Nbe/Model/LogRelTm_Back.v
+Nbe/Model/LogRelSb_Def.v
+Nbe/Model/LogRelSb_BasicFacts.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.v
 
 Nbe/Extraction/Eval.v
   Nbe/Model/LogRelTm_ClosedUnderPer.v\
   Nbe/Model/LogRelTm_Lift.v\
   Nbe/Model/LogRelTm_Back.v\
+  Nbe/Model/LogRelSb_Def.v\
+  Nbe/Model/LogRelSb_BasicFacts.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.v\
   Nbe/Extraction/Eval.v\
   Nbe/Extraction/Rb.v\
 Require Export Nbe.Model.Valid.
 Require Export Nbe.Model.Terminating.
 Require Export Nbe.Model.LogRel.
+Require Export Nbe.Model.Final.

Nbe/Model/Final.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.LogRel.
+
+
+(******************************************************************************
+ * Main
+ *)
+
+Corollary RelType_Refl: forall Gamma T DT denv,
+  Gamma |-- T ->
+  EvalCxt Gamma denv ->
+  EvalTm T denv DT ->
+  forall HDT : DT === DT #in# PerType,
+  Gamma ||- T #in# HDT
+.
+Proof.
+intros.
+apply RelType_ClosedForConversion with (T := TmSb T Sid).
+eapply Rel_Fundamental_Tp; eauto.
+apply RelSid; eauto.
+eauto.
+Qed.
+
+Corollary RelTerm_Refl: forall Gamma t T dt DT denv,
+  Gamma |-- t : T ->
+  EvalCxt Gamma denv ->
+  EvalTm T denv DT ->
+  EvalTm t denv dt ->
+  forall HDT : DT === DT #in# PerType,
+  Gamma ||- t : T #aeq# dt #in# HDT
+.
+Proof.
+intros.
+apply RelTerm_ClosedForConversion with (t := TmSb t Sid) (T := TmSb T Sid).
+eapply RelType_Refl; eauto.
+eauto.
+eapply Rel_Fundamental_Tm; eauto.
+apply RelSid; eauto.
+apply EQ_CONV with (A := T).
+eauto.
+eauto.
+Qed.
+
+(******************************************************************************
+ * Main
+ *)
+
+Fact Helper_HDT: forall Gamma T denv DT,
+  Gamma |-- T ->
+  EvalCxt Gamma denv ->
+  EvalTm T denv DT ->
+  DT === DT #in# PerType
+.
+Proof.
+intros.
+assert (Gamma |= T).
+apply Valid_for_WfTp.
+auto.
+
+clear_inversion H2.
+edestruct H4.
+apply ValEnv_from_WfCxt; eauto.
+program_simpl.
+renamer.
+compute_sth.
+Qed.
+Hint Resolve Helper_HDT.
+
+Theorem Nbe_Soundness: forall Gamma t T n,
+  Gamma |-- t : T -> Nbe T Gamma t n ->
+  Gamma |-- t === n : T
+.
+Proof.
+intros.
+clear_inversion H0.
+
+renamer.
+assert (DT_denv === DT_denv #in# PerType) as HDT by eauto.
+
+destruct RelTerm_Reify
+  with (Gamma := Gamma) (T := T) (DT := DT_denv) (DT' := DT_denv) (t := t) (dt := Dt_denv)
+    (HDT := HDT)
+; eauto.
+eapply RelType_Refl; eauto.
+eapply RelTerm_Refl; eauto.
+program_simpl.
+assert (x = n).
+eapply RbNf_deter; eauto.
+subst.
+auto.
+Qed.
+
+Corollary Nbe_Soundness': forall Gamma t T,
+  Gamma |-- t : T ->
+  exists n, Nbe T Gamma t n /\ Gamma |-- t === n : T
+.
+Proof.
+intros.
+destruct NBE_Terminating with (Gamma := Gamma) (t := t) (A := T); auto.
+exists x; split; auto.
+apply Nbe_Soundness; eauto.
+Qed.
+
+
+Corollary Nbe_NotConvertible: forall Gamma t t' T n n',
+  Gamma |-- t : T ->
+  Gamma |-- t' : T ->
+  ~ Gamma |-- t === t' : T ->
+  Nbe T Gamma t n ->
+  Nbe T Gamma t' n' ->
+  n' <> n
+.
+Proof.
+intros.
+
+intro Heq; subst.
+contradict H1.
+eapply EQ_TRANS.
+apply Nbe_Soundness; eauto.
+apply EQ_SYM.
+apply Nbe_Soundness; eauto.
+Qed.
+
+
+Corollary Nbe_DecLogic: forall Gamma t t' T,
+  Gamma |-- t : T ->
+  Gamma |-- t' : T ->
+  Gamma |-- t === t' : T \/ ~ Gamma |-- t === t' : T
+.
+Proof.
+intros.
+
+destruct Nbe_Soundness' with Gamma t T as [n]; auto.
+destruct Nbe_Soundness' with Gamma t' T as [n']; auto.
+program_simpl.
+destruct (Tm_eqdec n n').
+
+(* yes *)
+subst.
+left.
+eapply EQ_TRANS.
+eauto.
+eauto.
+
+(* no *)
+
+right.
+intro Heq.
+contradict n0.
+eapply NBE_Determined; eauto.
+Qed.
+
+

Nbe/Model/LogRelSb.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.
-
-(******************************************************************************
- * 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.
-
-(******************************************************************************
- * 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.
-Check RelTerm_ClosedForConversion.
-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.
-
-Print EvalTm.
-Print EQ_SBSEQ.
-(* 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.
-eapply SEXT.
-eapply SSEQ.
-eauto.
-eauto.
-eauto.
-auto.
-eauto.
-
-
-assert (Delta,, TmSb A SB |-- TmVar : TmSb A (Sseq SB Sup)) as HZZ7.
-eapply CONV.
-eapply HYP.
-eauto.
-eapply EQ_TP_SBSEQ.
-eauto.
-eauto.
-eauto.
-
-
-assert(Delta0 |-- TmSb TmVar (Sext Sid a) === a :TmSb (TmSb A (Sseq SB (Sups i))) Sid) as HZZZ5.
-eapply EQ_SBVAR.
-eauto.
-eapply RelType_implies_WfTp with (T := TmSb A (Sseq SB (Sups i)) ).
-eapply RelTerm_implies_RelType.
-eauto.
-auto.
-
-assert ( Delta0 |-- TmSb TmVar (Sext Sid a) === a
-   : TmSb A (Sseq (Sseq (Sseq SB (Sups i)) Sup) (Sext Sid a))) as HZZZ6.
-
-eapply EQ_CONV.
-eauto.
-eapply EQ_TP_TRANS.
-eapply EQ_TP_SBID.
-eapply RelType_implies_WfTp with (T := TmSb A (Sseq SB (Sups i)) ).
-eapply RelTerm_implies_RelType.
-eauto.
-eapply EQ_TP_SYM.
-eapply EQ_TP_CONG_SB.
-eauto.
-eauto.
-
-(**)
-
-eapply EQ_CONV.
-eapply EQ_TRANS.
-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_SB_FUN.
-eapply SSEQ.
-eauto.
-eauto.
-eauto.
-eauto.
-eapply EQ_REFL.
-auto.
-
-eapply EQ_TRANS.
-eapply EQ_CONG_FUN_E.
-eapply EQ_SBABS.
-eauto.
-eauto.
-eapply EQ_REFL.
-eauto.
-
-eapply EQ_TRANS.
-eapply EQ_FUN_Beta.
-eapply System.SB.
-eapply SEXT.
-eapply SSEQ.
-eauto.
-eauto.
-eauto.
-
-auto.
-
-eauto.
-
-
-eauto.
-
-eapply EQ_TRANS.
-eapply EQ_SBSEQ.
-unfold Ssing.
-eauto.
-
-auto.
-
-
-eapply SEXT.
-eapply SSEQ.
-eauto.
-eauto.
-eauto.
-auto. (*HZZ2*)
-auto.
-
-eapply EQ_CONV.
-eapply EQ_CONG_SB.
-
-unfold Ssing.
-eapply EQ_SB_TRANS.
-eapply EQ_SB_SEXT.
-eauto.
-
-eapply SEXT.
-eapply SSEQ.
-eauto.
-eapply SSEQ.
-eauto.
-eauto.
-eauto.
-auto.
-  
-eapply EQ_SB_CONG_SEXT.
-auto.
-eauto.
-
-eauto.
-eauto.
-
-unfold Ssing.
-auto.
-unfold Ssing.
-
-eapply EQ_TP_TRANS.
-eapply EQ_TP_SBSEQ.
-eauto.
-eapply SEXT.
-eauto.
-eauto.
-auto.
-eauto.
-
-
-eapply EQ_TP_SYM.
-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_TRANS.
-eapply EQ_SB_CONG_SEXT.
-eauto.
-eauto.
-
-
-assert (Delta0 |-- TmSb TmVar (Sext (Sups i) a) === a
-   : TmSb A (Sseq (Sseq SB Sup) (Sext (Sups i) a))) as HZZZ7.
-eapply EQ_CONV.
-eapply EQ_SBVAR.
-eauto.
-eauto.
-eauto.
-eauto.
-
-eauto.
-
-eapply EQ_SB_SYM.
-eapply EQ_SB_TRANS.
-eapply EQ_SB_SEXT.
-eauto.
-eapply SEXT.
-eauto.
-eauto.
-auto.
-
-eapply EQ_SB_CONG_SEXT.
-eapply EQ_SB_TRANS.
-eauto.
-eauto.
-eauto.
-
-assert (Delta0 |-- TmSb TmVar (Sext (Sups i) a) === a
-   : TmSb A (Sseq (Sseq SB Sup) (Sext (Sups i) a))) as HZZZ7.
-eapply EQ_CONV.
-eapply EQ_SBVAR.
-eauto.
-eauto.
-eauto.
-eauto.
-
-eauto.
-eauto.
-
-(***)
-
-eapply RelTerm_ClosedForConversion.
-eauto.
-eauto.
-eauto.
-eauto.
-
-Qed.
-
-
-Theorem Rel_Fundamental_Fun: forall Gamma A  B Delta SB denv DT DT' (HDT : DT === DT' #in# PerType),
-  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) ->
-  Gamma,, A |-- B ->
-  ( 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) ->
-  Delta ||-  [SB]:Gamma #aeq# denv ->
-  EvalTm (TmFun A B) denv DT ->
-  Delta ||- TmSb (TmFun A B) SB #in# HDT
-.
-Proof.
-intros.
-
-assert (Delta |-- [SB] : Gamma) by (eapply RelSb_wellformed; eauto).
-
-destruct HDT; try solve [clear_inversion H4].
-simpl.
-exists (TmSb A SB).
-exists (TmSb B (Sext (Sseq SB Sup) TmVar)).
-split.
-
-eapply EQ_TP_SB_FUN.
-eauto.
-auto.
-auto.
-
-split.
-eapply H0.
-eauto.
-clear_inversion H4.
-auto.
-
-(**)
-
-intros.
-
-rename i1 into HREC.
-rename e into HappDF.
-rename e0 into HappDF'.
-rename i into HDA.
-rename i2 into i.
-
-assert (Delta0 |-- a : TmSb (TmSb A SB) (Sups i)) as HYY1.
-eapply RelTerm_implies_WtTm; eauto.
-
-assert (Delta0 |-- TmSb (TmSb A SB) (Sups i) === TmSb A (Sseq SB (Sups i))) as HYY2.
-eapply EQ_TP_SBSEQ; eauto.
-
-rename H2 into Hgoal.
-
-assert (Delta0 |-- [Sext (Sseq SB (Sups i)) a] : Gamma,,A) as HYY3.
-eapply SEXT; eauto. 
-
-clear_inversion H4.
-renamer.
-
-assert ( [denv] === [denv] #in# Gamma) as HYY4.
-eapply RelSb_valenv.
-eauto.
-
-assert ( [Dext denv da] === [Dext denv da] #in# Gamma,,A ) as HYY5.
-econstructor 2.
-eauto.
-exists DA_denv.
-split; eauto.
-auto.
-
-assert (Delta0 ||- [Sseq SB (Sups i)] : Gamma #aeq# denv) as HYY6.
-eapply RelSb_ClosedUnderLift.
-eauto.
-eauto.
-
-assert (Delta0 ||- a : TmSb A (Sseq SB (Sups i)) #aeq# da #in# HDA) as HYY7.
-eapply RelTerm_ClosedForConversion.
-eauto.
-eauto.
-eauto.
-eauto.
-
-assert (Delta0 ||- [Sext (Sseq SB (Sups i)) a] : Gamma,,A #aeq# Dext denv da) as HYY8.
-econstructor 2; eauto.
-
-inversion Happ; subst.
-
-move Hgoal at bottom.
-specialize (Hgoal _ _ _ HYY8).
-specialize (Hgoal _ _ (HREC da da DB DB' PDA_denv HPA Hda Happ Happ') H11).
-
-
-assert (Delta ||- TmSb A SB #in# HDA) as HYYY1.
-eauto.
-
-(**)
-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.
-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.
-
-(**)
-
-
-eapply RelType_ClosedForConversion; eauto.
-
-Qed.
-
-
-
-
-Lemma fromDnv_subst: forall k Psi sigma Sigma, Psi |-- [sigma] : Sigma -> Psi |-- TmSb (fromDnv k) sigma === fromDnv k : TmNat.
-induction k.
-intros.
-simpl.
-eapply EQ_SBNAT0.
-eauto.
-
-intros.
-simpl.
-eapply EQ_TRANS.
-eapply EQ_CONV.
-eapply EQ_SBAPP.
-eauto.
-eapply NS.
-eauto.
-eauto.
-eapply EQ_TP_TRANS.
-eapply EQ_TP_CONG_SB.