Paweł Wieczorek avatar Paweł Wieczorek committed 4a005db

Splitted LogRelTm into smaller files

Comments (0)

Files changed (10)

 Nbe/Model/Interp.v
 Nbe/Model/Valid.v
 Nbe/Model/Terminating.v
-Nbe/Model/LogRelTm.v
+Nbe/Model/LogRelTm_Def.v
+Nbe/Model/LogRelTm_BasicFacts.v
+Nbe/Model/LogRelTm_ProofIrrelevance.v
+Nbe/Model/LogRelTm_ClosedForConversion.v
+Nbe/Model/LogRelTm_ClosedUnderPer.v
+Nbe/Model/LogRelTm_Lift.v
+Nbe/Model/LogRelTm_Back.v
 Nbe/Model/LogRelSb.v
 Nbe/Model/LogRel.v
 Nbe/Model.v
   Nbe/Model/Interp.v\
   Nbe/Model/Valid.v\
   Nbe/Model/Terminating.v\
-  Nbe/Model/LogRelTm.v\
+  Nbe/Model/LogRelTm_Def.v\
+  Nbe/Model/LogRelTm_BasicFacts.v\
+  Nbe/Model/LogRelTm_ProofIrrelevance.v\
+  Nbe/Model/LogRelTm_ClosedForConversion.v\
+  Nbe/Model/LogRelTm_ClosedUnderPer.v\
+  Nbe/Model/LogRelTm_Lift.v\
+  Nbe/Model/LogRelTm_Back.v\
   Nbe/Model/LogRelSb.v\
   Nbe/Model/LogRel.v\
   Nbe/Model.v\

Nbe/Model/LogRelTm.v

  *)
 Add Rec LoadPath "../../Nbe" as Nbe.
 
-Require Import Arith.
-Require Import Arith.Plus.
+Require Export Nbe.Model.LogRelTm_Def.
+Require Export Nbe.Model.LogRelTm_BasicFacts.
+Require Export Nbe.Model.LogRelTm_ProofIrrelevance.
+Require Export Nbe.Model.LogRelTm_ClosedForConversion.
+Require Export Nbe.Model.LogRelTm_ClosedUnderPer.
+Require Export Nbe.Model.LogRelTm_Lift.
+Require Export Nbe.Model.LogRelTm_Back.
 
-Require Import Program.
-Require Import Program.Tactics.
-Require Import Program.Equality.
-Require Import Setoid.
-Require Import Relations.Relation_Definitions.
-Require Import Classes.RelationClasses.
-
-
-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.
-
-(******************************************************************************
- * Additional definitions
- *)
-
-Fact CxtShift_type: forall Delta i Gamma T,
-  CxtShift Delta i Gamma ->
-  Gamma |-- T ->
-  Delta |-- TmSb T (Sups i)
-.
-Proof.
-intros.
-red in H.
-eauto.
-Qed.
-
-Lemma WtSb_SIDR: forall Gamma sb Delta,
-  Gamma |-- [Sseq sb Sid] : Delta ->
-  Gamma |-- [sb] : Delta
-.
-Proof.
-intros.
-remember (Sseq sb Sid).
-generalize dependent sb.
-induction H; intros;
-  try subst; try solve [clear_inversion Heqs].
-clear_inversion Heqs.
-clear_inversion H.
-eauto.
-Qed.
-
-Lemma WtSb_SUPR: forall Gamma sb Delta,
-  Gamma |-- [Sseq Sup sb] : Delta ->
-    exists A,  Gamma |-- [sb] : Delta,,A
-.
-Proof.
-intros.
-clear_inversion H.
-clear_inversion H5.
-eauto.
-Qed.
-
-Lemma WtSb_SUPL: forall Gamma sb Delta,
-  Gamma |-- [Sseq sb Sup] : Delta ->
-    exists Psi A, Gamma = (Psi,,A) /\ Psi |-- [sb] : Delta
-.
-Proof.
-intros.
-clear_inversion H.
-clear_inversion H3.
-eauto.
-Qed.
-
-Lemma WtSb_SIDL: forall Gamma sb Delta,
-  Gamma |-- [Sseq Sid sb] : Delta ->
-  Gamma |-- [sb] : Delta
-.
-Proof.
-intros.
-remember (Sseq Sid sb).
-generalize dependent sb.
-induction H; intros;
-  try subst; try solve [clear_inversion Heqs].
-clear_inversion Heqs.
-clear_inversion H0.
-eauto.
-Qed.
-
-
-
-
-(******************************************************************************
- * Helpers for Logical Relations
- *)
-
-Scheme PerType_dind := Induction for PerType Sort Prop.
-
-Reserved Notation "Gamma ||- A #in# X "
- (no associativity, at level 75, A, X at next level).
-
-Reserved Notation "Gamma ||- t : A #aeq# d #in# X"
- (no associativity, at level 75, A, X, t, d at next level).
-
-Fact PerType_inv_Dfun_DA: forall DT DT' DA DF DA' DF',
-  DT === DT' #in# PerType ->
-  DT = Dfun DA DF ->
-  DT' = Dfun DA' DF' ->
-  DA === DA' #in# PerType
-.
-do 7 intro.  
-auto_inversion_on H.
-intros.
-injection H5.
-injection H6.
-let Hr := fresh "Hr" in intro Hr; try rewrite <- Hr;
-let Hr := fresh "Hr" in intro Hr; try rewrite <- Hr;
-let Hr := fresh "Hr" in intro Hr; try rewrite <- Hr;
-let Hr := fresh "Hr" in intro Hr; try rewrite <- Hr.
-assumption.
-Defined.
-
-Fact PerType_inv_Dfun_DB: forall DT DT' DA DF DA' DF',
-  DT === DT' #in# PerType ->
-  DT = Dfun DA DF ->
-  DT' = Dfun DA' DF' ->
-  (forall a0 a1 DB0 DB1 PA, Interp DA PA -> a0 === a1 #in# PA -> App DF a0 DB0 -> App DF' a1 DB1 ->
-    DB0 === DB1 #in# PerType
-  )
-.
-do 7 intro.  
-auto_inversion_on H.
-do 12 intro.
-injection H5.
-injection H6.
-let Hr := fresh "Hr" in intro Hr; try rewrite <- Hr;
-let Hr := fresh "Hr" in intro Hr; try rewrite <- Hr;
-let Hr := fresh "Hr" in intro Hr; try rewrite <- Hr;
-let Hr := fresh "Hr" in intro Hr; try rewrite <- Hr.
-assumption.
-Defined.
-
-(******************************************************************************
- * Logical relations
- *
- * The relation RelType connects a judgement 'Gamma |-- T' with 
- * an element 'DT' from PerType's domain, such that reification of
- * 'DT' is convertible to A.
- *
- * Second relation is between a judgement 'Gamma |-- t : T' and
- * an element 'DT' from PerType's domain and an element 'dt' from
- * PER relation assigned to DT. Relation guards if reification of 'dt'
- * is convertible to 't'.
- *
- * Relation have to be defined on elements which belongs to PerType's
- * domains, we achieve this by structural recursion on the
- * proof 'DT === DT #in# PerType'. Shape of this proof should be irrelevant
- * for relation, we check this in 'Rel_ProofIrrelevance' lemma.
- *)
-
-Fixpoint RelType (Gamma:Cxt) (T:Tm) (DT DT':D) (HDT : DT === DT' #in# PerType) : Prop :=
-  match DT as _DT, DT' as _DT' return (DT = _DT -> DT' = _DT' -> Prop)
-    with
-
-    | Dnat, Dnat => fun _ _ =>
-      Gamma |-- T === TmNat
-
-    | Dunit, Dunit => fun _ _ =>
-      Gamma |-- T === TmUnit
-
-    | Dempty, Dempty => fun _ _ =>
-      Gamma |-- T === TmEmpty
-
-    | Dfun DA DF, Dfun DA' DF' => fun Heq Heq' => 
-      exists A F,
-        Gamma |-- T === TmFun A F /\
-        Gamma ||- A #in# (PerType_inv_Dfun_DA HDT Heq Heq') /\
-          (forall Delta i a da DB DB' PA (HPA : Interp DA PA)
-            (Hda : da === da #in# PA)
-            (Happ : App DF da DB) (Happ' : App DF' da DB'),
-            CxtShift Delta i Gamma ->
-            Delta ||- a : (TmSb A $ Sups i) #aeq# da #in# (PerType_inv_Dfun_DA HDT Heq Heq') ->
-            Delta ||- TmSb F (Sext (Sups i) a) #in# (PerType_inv_Dfun_DB HDT Heq Heq' HPA Hda Happ Happ')
-          )
-
-    | _, _ => fun _ _ =>
-      False
-
-  end (eq_refl DT) (eq_refl DT')
-  where "Gamma ||- A #in# HDT" := (RelType Gamma A HDT) 
-
-with RelTerm Gamma t T dt DT DT' (HDT : DT === DT' #in# PerType) : Prop :=
-  match DT as _DT, DT' as _DT' return (DT = _DT -> DT' = _DT' -> Prop)
-    with
-
-    | Dnat, Dnat => fun _ _ =>
-      dt === dt #in# PerNat /\
-      Gamma |-- T === TmNat /\
-      (forall Delta i,
-        CxtShift Delta i Gamma ->
-        exists v, RbNf (length Delta) (Ddown Dnat dt) v /\
-          Delta |-- TmSb t (Sups i) === v : TmNat 
-      ) 
-
-    | Dunit, Dunit => fun _ _ =>
-      dt === dt #in# PerUnit /\
-      Gamma |-- T === TmUnit /\
-      (forall Delta i,
-        CxtShift Delta i Gamma ->
-        exists v, RbNf (length Delta) (Ddown Dunit dt) v /\
-          Delta |-- TmSb t (Sups i) === v : TmUnit 
-      ) 
-
-    | Dempty, Dempty => fun _ _ =>
-      dt === dt #in# PerEmpty /\
-      Gamma |-- T === TmEmpty /\
-      (forall Delta i,
-        CxtShift Delta i Gamma ->
-        exists v, RbNf (length Delta) (Ddown Dempty dt) v /\
-          Delta |-- TmSb t (Sups i) === v : TmEmpty
-      ) 
-
-    | Dfun DA DF, Dfun DA' DF' => fun Heq Heq' =>
-      Gamma |-- t : T /\
-      exists A F PT,
-        Interp (Dfun DA DF) PT /\
-        dt === dt #in# PT /\
-        Gamma |-- T === TmFun A F /\
-        Gamma ||- A #in# (PerType_inv_Dfun_DA HDT Heq Heq') /\
-          (forall Delta i a da DB DB' PA (HPA : Interp DA PA)
-            (Hda : da === da #in# PA) (Happ : App DF da DB) (Happ' : App DF' da DB'),
-            CxtShift Delta i Gamma ->
-            Delta ||- a : (TmSb A $ Sups i) #aeq# da #in# (PerType_inv_Dfun_DA HDT Heq Heq') ->
-            exists dy, App dt da dy /\
-            Delta ||- TmApp (TmSb t (Sups i)) a : TmSb F (Sext (Sups i) a) #aeq# dy #in# (PerType_inv_Dfun_DB HDT Heq Heq' HPA Hda Happ Happ')
-          )
-
-    | _, _ => fun _ _ =>
-      False
-  end (eq_refl DT)  (eq_refl DT')
-
-where "Gamma ||- t : A #aeq# d #in# X" := (RelTerm Gamma t A d X)
-.
-
-(******************************************************************************
- * RelTerm implies RelType
- *
- * The logical relation between judgement 'Gamma |-- t : T' and 'dt #in# (Interp DT)'
- * should be satisfied only when relation between 'Gamma |-- T' and 'DT' holds.
- *)
-
-Fact RelTerm_implies_RelType: forall Gamma t T dt DT DT' (HDT : DT === DT' #in# PerType),
-  Gamma ||- t : T #aeq# dt #in# HDT ->
-  Gamma ||- T #in# HDT
-.
-Proof.
-intros.
-
-generalize dependent Gamma.
-generalize dependent t.
-generalize dependent T.
-generalize dependent dt.
-
-induction HDT using PerType_dind.
-
-intros.
-simpl in *; intros.
-program_simpl.
-
-intros.
-simpl in *.
-program_simpl.
-
-intros.
-simpl in *; intros.
-destruct H0 as [_H0 H0].
-destruct H0 as [A [F [? [? ?]]]].
-exists A F. repeat split; program_simpl; auto.
-program_simpl; auto.
-intros.
-edestruct H6 as [y]; eauto.
-program_simpl.
-eapply H. eauto.
-
-intros.
-simpl in *; intros.
-program_simpl.
-Qed.
-Hint Resolve RelTerm_implies_RelType.
-
-(******************************************************************************
- * 
- *)
-
-Fact RelTerm_has_Interp: forall Gamma t T dt DT DT' (HDT: DT === DT' #in# PerType),
-  Gamma ||- t : T #aeq# dt #in# HDT ->
-  exists PT, Interp DT PT 
-.
-Proof.
-intros.
-cut (Gamma ||- T #in# HDT); intros; eauto.
-Qed.
-Hint Resolve RelTerm_has_Interp.
-
-(******************************************************************************
- * RelTerm respects Interp
- *)
-
-Fact RelTerm_resp_Interp: forall Gamma t T dt DT DT' (HDT: DT === DT' #in# PerType) PT,
-  Gamma ||- t : T #aeq# dt #in# HDT ->
- Interp DT PT ->
- dt === dt #in# PT
-.
-Proof.
-intros.
-generalize dependent PT.
-induction HDT using PerType_dind; intros; simpl in *.
-(**)
-program_simpl; 
-clear_inversion H0;
-auto.
-(**)
-program_simpl; 
-clear_inversion H0;
-auto.
-(**)
-program_simpl.
-find_extdeters.
-apply H10.
-eauto.
-(**)
-program_simpl.
-clear_inversion H0.
-auto.
-Qed.
-Hint Resolve RelTerm_resp_Interp.
-
-(******************************************************************************
- * RelType implies type judgemement
- *)
-
-Fact RelType_implies_WfTp: forall Gamma T DT DT' (HDT : DT === DT' #in# PerType),
-  Gamma ||- T #in# HDT ->
-  Gamma |-- T
-.
-Proof.
-intros.
-induction HDT using PerType_dind; intros.
-
-simpl in H;eauto.
-simpl in H;eauto.
-simpl in H.
-program_simpl.
-eauto.
-
-simpl in H;eauto.
-Qed.
-Hint Resolve RelTerm_resp_Interp.
-
-Lemma SBID_inv: forall t T Gamma,
-  Gamma |-- TmSb t Sid : T ->
-  Gamma |-- t : T
-.
-Proof.
-intros.
-remember (TmSb t Sid).
-induction H; clear_inversion Heqt0.
-
-clear_inversion H.
-eapply CONV. eauto.
-eapply EQ_TP_SYM.
-eapply EQ_TP_SBID.
-eauto.
-eapply CONV.
-apply IHWtTm; eauto.
-eauto.
-Qed.
-Hint Resolve SBID_inv.
-
-(******************************************************************************
- * RelTerm implies term judgemement
- *)
-
-Fact RelTerm_implies_WtTm: forall Gamma t T dt DT DT' (HDT : DT === DT' #in# PerType),
-  Gamma ||- t : T #aeq# dt #in# HDT ->
-  Gamma |-- t : T
-.
-Proof.
-intros.
-induction HDT using PerType_dind; intros.
-(**)
-simpl in H; program_simpl.
-specialize (H1 Gamma 0).
-destruct H1. red; eauto.
-program_simpl.
-
-simpl in *.
-assert (Gamma |-- TmSb t Sid : TmNat).
-eapply WtTm_from_WtTmEq1; eauto.
-
-apply SBID_inv. 
-apply CONV with TmNat. auto.
-eauto.
-(**)
-simpl in H; program_simpl.
-specialize (H1 Gamma 0).
-destruct H1. red; eauto.
-program_simpl.
-
-simpl in *.
-assert (Gamma |-- TmSb t Sid : TmUnit).
-eapply WtTm_from_WtTmEq1; eauto.
-
-apply SBID_inv. 
-apply CONV with TmUnit. auto.
-eauto.
-(**)
-simpl in H.
-program_simpl.
-(**)
-simpl in H; program_simpl.
-specialize (H1 Gamma 0).
-destruct H1. red; eauto.
-program_simpl.
-
-simpl in *.
-assert (Gamma |-- TmSb t Sid : TmEmpty).
-eapply WtTm_from_WtTmEq1; eauto.
-
-apply SBID_inv. 
-apply CONV with TmEmpty. auto.
-eauto.
-Qed.
-
-(******************************************************************************
- * RelTerm implies type judgemement
- *)
-
-Fact RelTerm_implies_WfTp: forall Gamma t T dt DT DT' (HDT : DT === DT' #in# PerType),
-  Gamma ||- t : T #aeq# dt #in# HDT ->
-  Gamma |-- T
-.
-Proof.
-intros.
-eapply RelType_implies_WfTp.
-eapply RelTerm_implies_RelType.
-eauto.
-Qed.
-
-(******************************************************************************
- * Proof irrelevance for Logical Relations
- *
- * Shape of the proof 'DT === DT #in# PerType' is irrelevant for satisfability
- * of the relation.
- *)
-
-Theorem Rel_ProofIrrelevance: forall Gamma T DT DT' (HDT HDT': DT === DT' #in# PerType),
-  (Gamma ||- T #in# HDT ->  Gamma ||- T #in# HDT') /\
-  (forall t dt, Gamma ||- t : T #aeq# dt #in# HDT -> Gamma ||- t : T #aeq# dt #in# HDT')
-.
-Proof.
-(* We need stronger induction hypothesis, with equivalence, not just implication *)
-cut (forall Gamma T DT DT' (HDT : DT === DT' #in# PerType), 
-  (forall DT_ DT_', DT = DT_ -> DT' = DT_' -> forall (HDT_ : DT_ === DT_' #in# PerType),
-    Gamma ||- T #in# HDT <-> Gamma ||- T #in# HDT_) /\
-  (forall t dt, 
-  forall DT_ DT_', DT = DT_ -> DT' = DT_' -> forall (HDT_ : DT_ === DT_' #in# PerType),
-    Gamma ||- t : T #aeq# dt #in# HDT <-> Gamma ||- t : T #aeq# dt #in# HDT_) 
-).
-intros; edestruct H; eauto.
-split; intros.
-apply H0; eauto.
-apply H1; eauto.
-(**)
-intros until HDT.
-generalize dependent Gamma.
-generalize dependent T.
-induction HDT using PerType_dind; 
-  try solve [
-    intros; split; intros; split; intros;
-    induction HDT_ using PerType_dind; intros; try solve [try clear_inversion H0; try clear_inversion H1];
-     auto
-  ].
-
-renamer.
-rename i into HDAPerType.
-rename e into HAppDF.
-rename e0 into HAppDF'.
-rename i1 into HAppPerType.
-rename IHHDT into IH1.
-rename H into IH2.
-rename i0 into HPDA.
-
-split; intros.
-
-(* Dfun RelType *)
-induction HDT_ using PerType_dind; intros; try solve [clear_inversion H0].
-symmetry in H0.
-symmetry in H.
-clear_inversion H0.
-clear_inversion H.
-rename e into HAppDF2.
-rename e0 into HAppDF'2.
-renamer; intros.
-rename i1 into HAppPerType2.
-rename i2 into HPDA0.
-rename i into HDAPerType2.
-rename i0 into WEIRD.
-
-(* -> *)
-split. intro HRelT.
-
-simpl in HRelT.
-destruct HRelT as [A [F HRelT]].
-exists A F.
-program_simpl.
-repeat (split; eauto).
-(**)
-destruct IH1 with (T := A) (Gamma := Gamma) as [IH1a IH1b].
-apply IH1a; auto.
-(**)
-intros.
-move IH2 at bottom.
-specialize (IH2 da da DB DB' PA).
-specialize (IH2 HPA Hda Happ Happ').
-specialize (IH2 (TmSb F (Sext (Sups i) a))).
-specialize (IH2 Delta).
-destruct IH2 as [IH2a IH2b].
-apply IH2a; auto.
-apply H2; auto.
-move IH1 at bottom.
-specialize (IH1 (TmSb A (Sups i))).
-specialize (IH1 Delta).
-destruct IH1 as [IH1a IH1b].
-edestruct IH1b as [IH1b' IH1b'']; eauto.
-
-(* <- *)
-intro HRelT.
-
-simpl in HRelT.
-destruct HRelT as [A [F HRelT]].
-exists A F.
-program_simpl.
-repeat (split; eauto).
-(**)
-destruct IH1 with (T := A) (Gamma := Gamma) as [IH1a IH1b].
-edestruct IH1a as [IH1a' IH1a'']; eauto.
-(**)
-intros.
-move IH2 at bottom.
-specialize (IH2 da da DB DB' PA).
-specialize (IH2 HPA Hda Happ Happ').
-specialize (IH2 (TmSb F (Sext (Sups i) a))).
-specialize (IH2 Delta).
-destruct IH2 as [IH2a IH2b].
-specialize (IH2a DB DB' eq_refl eq_refl).
-specialize (IH2a (HAppPerType2 da da DB DB' PA HPA Hda Happ Happ')).
-destruct (IH2a) as [IH2a' IH2a''].
-
-apply IH2a''; auto.
-apply H2; auto.
-move IH1 at bottom.
-specialize (IH1 (TmSb A (Sups i))).
-specialize (IH1 Delta).
-destruct IH1 as [IH1a IH1b].
-apply IH1b; auto.
-
-(* Dfun RelType *)
-induction HDT_ using PerType_dind; intros; try solve [clear_inversion H0].
-symmetry in H0.
-symmetry in H.
-clear_inversion H0.
-clear_inversion H.
-rename e into HAppDF2.
-rename e0 into HAppDF'2.
-renamer; intros.
-rename i1 into HAppPerType2.
-rename i2 into HPDA0.
-rename i into HDAPerType2.
-rename i0 into WEIRD.
-split.
-
-(* -> *)
-intro HRelT.
-
-simpl in HRelT.
-destruct HRelT as [HDeriv [A [F [PT HRelT]]]].
-split; auto.
-exists A F PT.
-program_simpl.
-repeat (split; eauto).
-(**)
-destruct IH1 with (T := A) (Gamma := Gamma) as [IH1a IH1b].
-apply IH1a; auto.
-(**)
-intros.
-edestruct H4 as [dy]; eauto.
-destruct IH1 with (T := TmSb A (Sups i)) (Gamma := Delta) as [IH1a IH1b].
-specialize (IH1b a da DA DA' eq_refl eq_refl).
-specialize (IH1b HDAPerType2).
-destruct IH1b as [IH1b' IH1b''].
-apply IH1b''.
-auto.
-
-destruct H7.
-exists dy. split; auto.
-
-move IH2 at bottom.
-specialize (IH2 da da DB DB' PA).
-specialize (IH2 HPA Hda Happ Happ').
-specialize (IH2 (TmSb F (Sext (Sups i) a))).
-specialize (IH2 Delta).
-destruct IH2 as [IH2a IH2b].
-apply IH2b; auto.
-eauto.
-
-(* <- *)
-intro HRelT.
-
-simpl in HRelT.
-destruct HRelT as [HDeriv [A [F [PT HRelT]]]].
-split; auto.
-exists A F PT.
-program_simpl.
-repeat (split; eauto).
-(**)
-destruct IH1 with (T := A) (Gamma := Gamma) as [IH1a IH1b].
-edestruct IH1a as [IH1a' IH1a'']; eauto.
-(**)
-intros.
-edestruct H4 as [dy]; eauto.
-destruct IH1 with (T := TmSb A (Sups i)) (Gamma := Delta) as [IH1a IH1b].
-apply IH1b; auto. eauto.
-destruct H7.
-exists dy. split; auto.
-move IH2 at bottom.
-specialize (IH2 da da DB DB' PA).
-specialize (IH2 HPA Hda Happ Happ').
-specialize (IH2 (TmSb F (Sext (Sups i) a))).
-specialize (IH2 Delta).
-destruct IH2 as [IH2a IH2b].
-specialize (IH2b ( TmApp (TmSb t (Sups i)) a) dy DB DB' eq_refl eq_refl).
-specialize (IH2b (HAppPerType2 da da DB DB' PA HPA Hda Happ Happ')).
-destruct IH2b as [IH2b' IH2b''].
-apply IH2b''; auto.
-eauto.
-Qed.
-
-(******************************************************************************
- * Proof irrelevance for Logical Relations (unpacked)
- *)
-
-Remark RelType_ProofIrrelevance: forall Gamma T DT DT' (HDT HDT': DT === DT' #in# PerType),
-  (Gamma ||- T #in# HDT ->  Gamma ||- T #in# HDT')
-.
-Proof.
-intros.
-edestruct Rel_ProofIrrelevance; eauto.
-Qed.
-
-Remark RelTerm_ProofIrrelevance: forall Gamma T DT DT' (HDT HDT': DT === DT' #in# PerType),
-  (forall t dt, Gamma ||- t : T #aeq# dt #in# HDT -> Gamma ||- t : T #aeq# dt #in# HDT')
-.
-Proof.
-intros.
-edestruct Rel_ProofIrrelevance; eauto.
-Qed.
-
-(******************************************************************************
- * Closure under conversion
- *)
-
-Theorem ClosedForConversion: forall Gamma T DT DT' (HDT: DT === DT' #in# PerType),
-  Gamma ||- T #in# HDT -> forall T',
-  Gamma |-- T === T' ->
-  (Gamma ||- T' #in# HDT) /\
-  (forall dt t t', Gamma ||- t : T #aeq# dt #in# HDT ->  Gamma |-- t === t' : T ->  Gamma ||- t' : T' #aeq# dt #in# HDT)
-.
-Proof.
-do 5 intro.
-generalize dependent Gamma.
-generalize dependent T.
-induction HDT using PerType_dind; intros.
-
-
-(* Dnat *)
-simpl in *; program_simpl.
-repeat split; eauto; intros.
-decompose record H1.
-eauto.
-decompose record H1.
-edestruct H7; eauto.
-exists x. program_simpl; repeat split.
-assumption.
-eapply EQ_TRANS; eauto using H8.
-eapply EQ_CONV; eauto.
-
-(* Dunit *)
-simpl in *.
-repeat split; eauto; intros.
-decompose record H1.
-eauto.
-decompose record H1.
-edestruct H7; eauto.
-exists x. program_simpl; repeat split.
-assumption.
-eapply EQ_TRANS; eauto using H8.
-eapply EQ_CONV; eauto.
-
-(* Dfun *)
-
-repeat split.
-simpl in *.
-
-destruct H0 as [A [F [? ?]]].
-exists A F.
-program_simpl.
-repeat split; auto.
-eapply EQ_TP_TRANS; eauto using H0.
-
-(**)
-
-eauto.
-
-(**)
-
-intros.
-renamer.
-rename i into HDA.
-rename i1 into HDB.
-rename i0 into HPA.
-intros.
-
-simpl.
-rename H0 into K_T.
-rename H2 into K_t.
-
-set (H_t := K_t).
-specialize (H_t).
-simpl in H_t.
-destruct H_t as [_H_t H_t].
-destruct H_t as [A [F [PT ?]]].
-program_simpl.
-renamer.
-intros.
-exists A F PT.
-repeat split; auto.
-eapply EQ_TP_TRANS; eauto using H1.
-
-intros.
-find_extdeters.
-close_extdeters.
-close_doms.
-renamer; intros.
-
-edestruct (H6 Delta i a da DB DB' PDA0 HPA1 Hda Happ Happ') as [dy ?]; eauto.
-exists dy.
-program_simpl.
-repeat split; auto.
-
-move H at bottom.
-specialize (H da da DB DB' PDA0).
-
-specialize (H HPA1 Hda).
-specialize (H Happ Happ').
-specialize (H (TmSb F (Sext (Sups i) a)) Delta).
-
-assert (Delta ||- TmSb F (Sext (Sups i) a) #in# HDB da da DB DB' PDA0 HPA1 Hda Happ Happ' ).
-eapply RelTerm_implies_RelType; eauto.
-specialize (H H15).
-specialize (H (TmSb F (Sext (Sups i) a))).
-
-assert (Delta |-- TmSb F (Sext (Sups i) a) === TmSb F (Sext (Sups i) a)).
-eapply EQ_TP_REFL.
-
-eapply RelType_implies_WfTp.
-eauto.
-
-specialize (H H16).
-destruct H.
-specialize (H17 dy (TmApp (TmSb t (Sups i)) a)).
-specialize (H17 (TmApp (TmSb t' (Sups i)) a)).
-apply H17.
-auto.
-
-(**)
-
-assert (Gamma |-- A /\ Gamma,,A |-- F).
-eapply Inversion_FUN_E.
-eauto.
-destruct H18.
-
-
-
-assert (Delta |-- a : TmSb A (Sups i)).
-eapply RelTerm_implies_WtTm.
-eauto.
-
-assert (Delta |-- TmSb A (Sups i)).
-eapply WfTp_from_WtTm.
-eauto.
-
-assert (Delta |-- a : TmSb (TmSb A (Sups i)) Sid).
-eapply CONV.
-eauto.
-eapply EQ_TP_SYM.
-eapply EQ_TP_SBID.
-auto.
-
-assert (Delta,, TmSb A (Sups i) |-- TmVar : TmSb A (Sseq (Sups i) Sup)).
-eapply CONV.
-eapply HYP.
-eauto.
-eauto.
-
-assert (Delta |--  [Sext Sid a]: Delta,,TmSb A (Sups i)) by eauto.
-
-
-assert (Delta |-- TmSb F (Sext (Sups i) a) === TmSb (TmSb F (Sext (Sups (S i)) TmVar)) (Ssing a)).
-
-
-eapply EQ_TP_SYM.
-eapply EQ_TP_TRANS.
-eapply EQ_TP_SBSEQ.
-unfold Ssing.
-eauto.
-eapply SEXT.
-simpl.
-eapply SSEQ.
-eapply SUP.
-assumption.
-apply H7.
-eauto.
-simpl.
-eauto.
-eauto.
-eapply EQ_TP_CONG_SB.
-unfold Ssing.
-eapply EQ_SB_TRANS.
-eapply EQ_SB_SEXT.
-eauto.
-eapply SEXT.
-simpl.
-eapply SSEQ.
-eauto.
-apply H7.
-eauto.
-simpl.
-auto.
-
-assert (   Delta,, TmSb A (Sups i) |--  [Sups (S i)]=== [Sseq Sup (Sups i)]:Gamma).
-apply Sups_tail.
-simpl.
-eapply SSEQ.
-eauto.
-eauto.
-
-eapply EQ_SB_CONG_SEXT.
-eapply EQ_SB_TRANS.
-
-simpl.
-eapply EQ_SB_COMM.
-eauto.
-eauto.
-eauto.
-
-eapply EQ_SB_TRANS.
-eapply EQ_SB_CONG_SSEQ.
-eapply EQ_SB_SUP.
-eauto.
-eauto.
-eauto.
-
-eapply EQ_SB_REFL.
-eauto.
-eauto.
-eauto.
-
-eapply EQ_CONV.
-eapply EQ_SBVAR.
-eauto.
-eauto.
-eauto.
-
-eapply EQ_TP_TRANS.
-eapply EQ_TP_SBSEQ.
-eauto.
-eauto.
-eauto.
-eapply EQ_TP_CONG_SB.
-eapply EQ_SB_SYM.
-simpl.
-
-eapply EQ_SB_TRANS.
-eapply EQ_SB_COMM.
-eauto.
-eauto.
-eauto.
-
-eapply EQ_SB_CONG_SSEQ.
-eapply EQ_SB_SUP.
-eauto.
-eauto.
-eauto.
-eapply EQ_SB_REFL.
-eauto.
-eauto.
-eauto.
-
-(**)
-
-eapply EQ_CONV.
-eapply EQ_CONG_FUN_E.
-eapply EQ_CONV.
-eapply EQ_CONG_SB.
-eapply EQ_SB_REFL.
-eauto.
-eauto.
-eapply EQ_TP_TRANS.
-eapply EQ_TP_CONG_SB.
-eapply EQ_SB_REFL.
-eauto.
-eauto.
-eauto.
-eapply EQ_REFL.
-eauto.
-
-(**)
-
-auto.
-
-(* Dempty *)
-simpl in *.
-repeat split; eauto; intros.
-decompose record H1.
-eauto.
-decompose record H1.
-edestruct H7; eauto.
-exists x. program_simpl; repeat split.
-assumption.
-eapply EQ_TRANS; eauto using H8.
-eapply EQ_CONV; eauto.
-Qed.
-
-(******************************************************************************
- * Closure under conversion (unpacking)
- *)
-
-Corollary RelType_ClosedForConversion: forall Gamma T DT DT' (HDT: DT === DT' #in# PerType) T',
-  Gamma ||- T #in# HDT ->
-  Gamma |-- T === T' ->
-  (Gamma ||- T' #in# HDT)
-.
-Proof.
-intros.
-edestruct ClosedForConversion; eauto.
-Qed.
-
-Corollary RelTerm_ClosedForConversion: forall Gamma T DT DT' (HDT: DT === DT' #in# PerType) T' dt t t',
-  Gamma ||- T #in# HDT -> 
-  Gamma |-- T === T' ->
-  Gamma ||- t : T #aeq# dt #in# HDT ->  Gamma |-- t === t' : T ->  Gamma ||- t' : T' #aeq# dt #in# HDT
-.
-Proof.
-intros.
-edestruct ClosedForConversion; eauto.
-Qed.
-
-(******************************************************************************
- * Closure under PERs
- *)
-
-Lemma Reflects_same: forall dt dt' DT PT n v,
-  DT === DT #in# PerType ->
-  Interp DT PT ->
-  dt === dt' #in# PT ->
-  RbNf n (Ddown DT dt) v ->
-  RbNf n (Ddown DT dt') v
-.
-Proof.
-intros.
-
-assert (Ddown DT dt === Ddown DT dt' #in# PerNf).
-eapply Reify_Characterization; eauto.
-clear_inversion H3.
-destruct (H4 n) as [v'].
-program_simpl.
-assert (v = v').
-eapply RbNf_deter; eauto.
-subst.
-assumption.
-Qed.  
-Hint Resolve Reflects_same.
-
-
-Theorem ClosedUnderPer: forall Gamma T DT DT' (HDT : DT === DT' #in# PerType),
-  Gamma ||- T #in# HDT -> 
-  forall DT'' (HDT' : DT' === DT'' #in# PerType),
-  Gamma ||- T #in# HDT' /\
- (forall t dt dt' PT, Gamma ||- t : T #aeq# dt #in# HDT -> dt === dt' #in# PT -> Interp DT PT ->
-   Gamma ||- t : T #aeq# dt' #in# HDT').
-
-Proof.
-(* Stronger induction hypothesis is required *)
-cut (forall Gamma T DT DT' (HDT : DT === DT' #in# PerType),
-  forall DT'' (HDT' : DT' === DT'' #in# PerType), (Gamma ||- T #in# HDT <-> Gamma ||- T #in# HDT')
-/\
-  (forall t dt dt' PT, dt === dt' #in# PT -> Interp DT PT ->
-    (Gamma ||- t : T #aeq# dt #in# HDT <-> Gamma ||- t : T #aeq# dt' #in# HDT'))
-).
-intros.
-specialize (H Gamma T DT DT' HDT DT'' HDT').
-program_simpl.
-repeat (split; auto).
-apply H.
-auto.
-
-intros.
-eapply H1; eauto.
-(**)
-
-intros until HDT.
-cut (DT' = DT'); auto.
-generalize DT' at 1 3 5 7 as DT'_.
-generalize dependent Gamma.
-generalize dependent T.
-(* Theorem for RelType for base types are solved by simple destruction and inversion! *)
-induction HDT using PerType_dind; split; intros;
-  try solve [
-    destruct HDT'; try solve [ clear_inversion H ];
-    split; auto
-      ].
-
-(* RelTerm Dnat *)
-
-destruct HDT'; try solve [clear_inversion H ].
-clear_inversion H1.
-
-split; intro;
-close_doms; auto; split; auto; intros;
-split; intros; simpl in *; program_simpl; auto;
-edestruct H6 as [v]; program_simpl; eauto.
-
-(* <- *)
-
-exists v. split; auto.
-apply Reflects_same with dt' PerNat; auto.
-symmetry; auto.
-
-(* RelTerm Dunit *)
-
-destruct HDT'; try solve [clear_inversion H ].
-clear_inversion H1.
-
-split; intro;
-close_doms; auto; split; auto; intros;
-split; intros; simpl in *; program_simpl; auto;
-edestruct H6 as [v]; program_simpl; eauto.
-
-(* RelType Dfun  *)
-
-renamer.
-rename i into HDA.
-rename i0 into HPDA.
-rename i1 into H_PDB.
-destruct HDT'; try solve [clear_inversion H0].
-clear_inversion H0.
-renamer.
-rename i0 into HPDA'.
-rename i1 into H_PDB'.
-rename i into HDA'.
-rename e1 into e'.
-rename e2 into e0'.
-
-(* ->  *)
-
-split; intro HS.
-simpl in HS.
-destruct HS as [A [F [HS1 [HS2 HS3 ]]]].
-simpl. exists A F.
-repeat (split; auto).
-
-specialize (IHHDT A Gamma _ eq_refl).
-edestruct IHHDT as [IHHDT_Type IHHDT_Term].
-(*specialize (IHHDT_Type _ HDA').*)
-apply IHHDT_Type; auto.
-
-(**)
-
-intros.
-renamer.
-assert (Interp DA' PDA) by (eapply Interp_resp_PerType; eauto).
-find_extdeters.
-close_doms.
-
-destruct e with da as [DB_].
-eauto.
-
-destruct e' with da as [DB_'].
-eauto.
-
-
-specialize (HS3 Delta i a da DB_ DB_' PDA).
-specialize (HS3 HPDA).
-assert (da === da #in# PDA) as HdadaPDA.
-apply H3.
-auto.
-specialize (HS3 HdadaPDA H9 H10 H0).
-
-assert ( Delta ||- a : TmSb A (Sups i) #aeq# da #in# HDA ) as HS1_P.
-specialize (IHHDT (TmSb A (Sups i)) Delta _ eq_refl).
-edestruct IHHDT as [IHHDT_Type IHHDT_Term].
-move IHHDT_Term at bottom.
-specialize (IHHDT_Term a da da PDA HdadaPDA HPDA).
-apply IHHDT_Term.
-eauto.
-
-specialize (HS3 HS1_P).
-
-move H at bottom.
-
-assert (DB_' = DB) by eauto 2; subst.
-
-
-specialize (H _ _ _ _ PDA HPDA HdadaPDA H9 H10).
-specialize (H ( TmSb F (Sext (Sups i) a))).
-specialize (H Delta _ eq_refl _ (H_PDB' da da DB DB' PDA'0 HPA Hda Happ Happ' ) ).
-destruct H.
-eapply H; auto.
-
-(* <- *)
-
-simpl in HS.
-destruct HS as [A [F [HS1 [HS2 HS3 ]]]].
-simpl. exists A F.
-repeat (split; auto).
-
-specialize (IHHDT A Gamma _ eq_refl).
-edestruct IHHDT as [IHHDT_Type IHHDT_Term].
-(*specialize (IHHDT_Type _ HDA').*)
-apply IHHDT_Type; eauto.
-
-(**)
-
-intros.
-renamer.
-assert (Interp DA PDA').
-eapply Interp_resp_PerType.
-eauto 1.
-symmetry; auto.
-
-find_extdeters.
-close_doms.
- 
-destruct e' with da as [DB_].
-eauto.
-
-destruct e0' with da as [DB_'].
-eauto.
-
-specialize (HS3 Delta i a da DB_ DB_' PDA').
-specialize (HS3 HPDA').
-assert (da === da #in# PDA') as HdadaPDA'.
-eauto.
-
-assert (DB' = DB_) by eauto 2; subst.
-
-specialize (HS3 HdadaPDA' H9 H10 H0).  
-
-assert ( Delta ||- a : TmSb A (Sups i) #aeq# da #in# HDA' ) as HS1_P.
-specialize (IHHDT (TmSb A (Sups i)) Delta _ eq_refl).
-edestruct IHHDT as [IHHDT_Type IHHDT_Term].
-move IHHDT_Term at bottom.
-specialize (IHHDT_Term a da da _ HdadaPDA' H2).
-apply IHHDT_Term.
-eauto.
-
-
-specialize (HS3 HS1_P).
-
-move H at bottom.
-
-specialize (H _ _ _ _ PDA0 HPA Hda Happ Happ').
-specialize (H ( TmSb F (Sext (Sups i) a))).
-specialize (H Delta _ eq_refl).
-specialize (H _ ( H_PDB' da da DB_ DB_' PDA' HPDA' HdadaPDA' H9 H10 )).
-destruct H.
-eapply H; auto.
-
-(* RelTerm Dfun *)
-
-renamer.
-rename i into HDA.
-rename i0 into HPDA.
-rename i1 into H_PDB.
-destruct HDT'; try solve [clear_inversion H0].
-clear_inversion H0.
-renamer.
-rename i0 into HPDA'.
-rename i1 into H_PDB'.
-rename i into HDA'.
-rename e1 into e'.
-rename e2 into e0'.
-
-(* ->  *)
-
-split; intro HS.
-simpl in HS.
-destruct HS as [? [A [F [Pfun [HS1 [HS2 [HS3 [HS4 HS5]]]]]]]].
-simpl. split; auto. exists A F Pfun.
-repeat (split; auto).
-
-apply Interp_resp_PerType with (DA := Dfun DA DF); auto.
-eapply PerType_arr; eauto 4.
-find_extdeters.
-close_extdeters.
-eauto.
-
-(**)
-
-specialize (IHHDT A Gamma _ eq_refl).
-edestruct IHHDT as [IHHDT_Type IHHDT_Term].
-(*specialize (IHHDT_Type _ HDA').*)
-apply IHHDT_Type; auto.
-
-(**)
-
-intros.
-renamer.
-assert (Interp DA' PDA) by (eapply Interp_resp_PerType; eauto).
-find_extdeters.
-close_doms.
-
-destruct e with da as [DB_].
-eauto.
-
-destruct e' with da as [DB_'].
-eauto.
-
-
-specialize (HS5 Delta i a da DB_ DB_' PDA).
-specialize (HS5 HPDA).
-assert (da === da #in# PDA) as HdadaPDA.
-eauto.
-specialize (HS5 HdadaPDA H15 H16 H3).
-
-assert ( Delta ||- a : TmSb A (Sups i) #aeq# da #in# HDA ) as HS1_P.
-specialize (IHHDT (TmSb A (Sups i)) Delta _ eq_refl).
-edestruct IHHDT as [IHHDT_Type IHHDT_Term].
-move IHHDT_Term at bottom.
-specialize (IHHDT_Term a da da PDA HdadaPDA HPDA).
-apply IHHDT_Term.
-eauto.
-
-specialize (HS5 HS1_P).
-clear_inversion H2.
-
-clear_inversion H1.
-find_extdeters.
-close_extdeters.
-specialize (H2 da da H17).
-destruct H2 as [y0 [y1 [Y HY]]].
-destruct HY as [HY [Hy0 [Hy1 HyyY]]].
-destruct HS5 as [dy HS6].
-program_simpl.
-assert (dy = y0) by eauto 2; subst.
-exists y1.
-split; auto.
-
-move H at bottom.
-
-assert (DB_' = DB) by eauto 2; subst.
-
-
-specialize (H _ _ _ _ PDA HPDA HdadaPDA H15 H16).
-specialize (H ( TmSb F (Sext (Sups i) a))).
-specialize (H Delta _ eq_refl _ (H_PDB' da da DB DB' PDA'0 HPA Hda Happ Happ' ) ).
-destruct H.
-eapply H25.
-eauto.
-eauto.
-eauto.
-
-(* <- *)
-
-simpl in HS.
-destruct HS as [? [A [F [Pfun [HS1 [HS2 [HS3 [HS4 HS5]]]]]]]].
-simpl. split; auto. exists A F Pfun.
-
-assert (Interp (Dfun DA DF) Pfun).
-apply Interp_resp_PerType with (DA := Dfun DA' DF'); auto.
-symmetry.
-eapply PerType_arr; eauto 4.
-
-
-repeat (split; auto).
-find_extdeters.
-close_extdeters.
-eauto.
-
-(**)
-
-specialize (IHHDT A Gamma _ eq_refl).
-edestruct IHHDT as [IHHDT_Type IHHDT_Term].
-(*specialize (IHHDT_Type _ HDA').*)
-apply IHHDT_Type; eauto.
-
-(**)
-
-intros.
-renamer.
-
-assert (Interp DA PDA').
-eapply Interp_resp_PerType.
-eauto 1.
-symmetry; auto.
-
-find_extdeters.
-close_doms.
- 
-destruct e' with da as [DB_].
-eauto.
-
-destruct e0' with da as [DB_'].
-eauto.
-
-assert (DB' = DB_) by eauto 2; subst.
-
-specialize (HS5 Delta i a da DB_ DB_' PDA').
-specialize (HS5 HPDA').
-assert (da === da #in# PDA') as HdadaPDA'.
-eauto.
-specialize (HS5 HdadaPDA' H16 H17 H4).
-
-
-assert ( Delta ||- a : TmSb A (Sups i) #aeq# da #in# HDA' ) as HS1_P.
-specialize (IHHDT (TmSb A (Sups i)) Delta _ eq_refl).
-edestruct IHHDT as [IHHDT_Type IHHDT_Term].
-move IHHDT_Term at bottom.
-specialize (IHHDT_Term a da da _ HdadaPDA' H6).
-eauto.
-apply IHHDT_Term.
-eauto.
-
-
-specialize (HS5 HS1_P).
-clear_inversion H2.
-clear_inversion H1.
-find_extdeters.
-close_extdeters.
-specialize (H2 da da H23).
-destruct H2 as [y0 [y1 [Y HY]]].
-destruct HY as [HY [Hy0 [Hy1 HyyY]]].
-destruct HS5 as [dy HS6].
-program_simpl.
-assert (dy = y1) by eauto 2; subst.
-exists y0.
-split; auto.
-
-move H at bottom.
-
-specialize (H _ _ _ _ _ HPA Hda Happ Happ').
-specialize (H ( TmSb F (Sext (Sups i) a))).
-specialize (H Delta _ eq_refl _ (H_PDB' da da _ _ PDA' HPDA' HdadaPDA' H16 H17 ) ).
-destruct H.
-eapply H28.
-eauto.
-eauto.
-eauto.
-
-(* RelTerm Dempty *)
-
-destruct HDT'; try solve [clear_inversion H ].
-clear_inversion H1.
-
-split; intro;
-close_doms; auto; split; auto; intros;
-split; intros; simpl in *; program_simpl; auto;
-edestruct H6 as [v]; program_simpl; eauto.
-
-(* <- *)
-
-exists v. split; auto.
-apply Reflects_same with dt' PerEmpty; auto.
-symmetry; auto.
-
-Qed.
-
-
-(***************************************************************************
- * Unpacking and helpers.
- *)
-
-Corollary RelType_ClosedUnderPer: forall Gamma T DT DT' (HDT : DT === DT' #in# PerType),
-  forall DT'' (HDT' : DT' === DT'' #in# PerType),
-  Gamma ||- T #in# HDT -> 
-  Gamma ||- T #in# HDT'
-.
-Proof.
-intros.
-edestruct ClosedUnderPer; eauto.
-Qed.
-
-Corollary RelTerm_ClosedUnderPer: forall Gamma T DT DT' (HDT : DT === DT' #in# PerType),
-  forall DT'' (HDT' : DT' === DT'' #in# PerType),
-  forall t dt dt' PT,
-   Gamma ||- t : T #aeq# dt #in# HDT -> dt === dt' #in# PT -> Interp DT PT ->
-   Gamma ||- t : T #aeq# dt' #in# HDT'
-.
-Proof.
-intros.
-destruct ClosedUnderPer with (Gamma := Gamma) (T := T) (DT := DT) (DT' := DT') (HDT := HDT) (DT'' := DT'') (HDT' := HDT').
-eapply RelTerm_implies_RelType.
-apply H.
-eauto.
-Qed.
-
-Corollary RelTerm_ClosedUnderPer': forall Gamma T DT DT' (HDT : DT === DT' #in# PerType),
-  forall t dt dt' PT,
-   Gamma ||- t : T #aeq# dt #in# HDT -> dt === dt' #in# PT -> Interp DT PT ->
-   Gamma ||- t : T #aeq# dt' #in# HDT
-.
-Proof.
-intros.
-assert (DT' === DT #in# PerType ) as HDT' by (symmetry; auto).
-
-destruct ClosedUnderPer with (Gamma := Gamma) (T := T) (DT := DT) (DT' := DT') (HDT := HDT) (DT'' := DT) (HDT' := HDT'); auto.
-eapply RelTerm_implies_RelType.
-apply H.
-
-destruct ClosedUnderPer with (Gamma := Gamma) (T := T) (DT := DT') (DT' := DT) (HDT := HDT') (DT'' := DT') (HDT' := HDT); auto.
-eauto.
-Qed.
-
-Corollary RelTerm_ClosedUnderPer'': forall Gamma T DT DT' (HDT : DT === DT' #in# PerType),
-  forall t dt DT'' (HDT' : DT' === DT'' #in# PerType),
-   Gamma ||- t : T #aeq# dt #in# HDT ->
-   Gamma ||- t : T #aeq# dt #in# HDT'
-.
-Proof.
-intros.
-
-destruct ClosedUnderPer with (Gamma := Gamma) (T := T) (DT := DT) (DT' := DT') (HDT := HDT) (DT'' := DT'') (HDT' := HDT'); auto.
-eapply RelTerm_implies_RelType.
-apply H.
-
-assert (exists PT, Interp DT PT) as HX1.
-eapply RelTerm_has_Interp.
-eauto.
-
-destruct HX1 as [PT HPT].
-
-assert (dt === dt #in# PT) as HX2.
-eapply RelTerm_resp_Interp.
-eauto.
-auto.
-
-eapply H1.
-eauto.
-eauto.
-auto.
-Qed.
-
-
-Lemma RelType_ClosedUnderPer_sym: forall Delta T DT DT'
-  (HDT1 : DT === DT' #in# PerType) (HDT2: DT' === DT #in# PerType),
-Delta ||- T #in# HDT1 ->
-Delta ||- T #in# HDT2
-.
-Proof.
-intros.
-
-assert (DT' === DT' #in# PerType) as HX1.
-eapply PER_Transitive with DT.
-symmetry; auto.
-auto.
-
-assert (Delta ||- T #in# HX1) as HX2.
-eapply RelType_ClosedUnderPer.
-eauto.
-
-eapply RelType_ClosedUnderPer.
-eauto.
-Qed.
-
-Lemma RelType_ClosedUnderPer_right: forall Delta T DT DT' DT'' 
-  (HDT1 : DT === DT' #in# PerType) (HDT2: DT === DT'' #in# PerType),
-Delta ||- T #in# HDT1 ->
-Delta ||- T #in# HDT2
-.
-Proof.
-intros.
-
-assert (DT' === DT'' #in# PerType) as HX1.
-apply PER_Transitive with DT.
-symmetry; auto.
-auto.
-
-assert (Delta ||- T #in# HX1 ) as HX2.
-eapply RelType_ClosedUnderPer.
-eauto.
-
-assert (DT'' === DT #in# PerType ) as HX3.
-symmetry; auto.
-
-assert (Delta ||- T #in# HX3 ) as HX4.
-eapply RelType_ClosedUnderPer.
-eauto.
-
-eapply RelType_ClosedUnderPer_sym.
-eauto.
-Qed.
-
-Lemma RelTerm_ClosedUnderPer_sym: forall Delta t T DT DT' dt dt' PT
-  (HDT1 : DT === DT' #in# PerType) (HDT2: DT' === DT #in# PerType),
-  dt === dt' #in# PT -> Interp DT PT ->
-Delta ||- t : T #aeq# dt #in# HDT1 ->
-Delta ||- t : T #aeq# dt' #in# HDT2
-.
-Proof.
-intros.
-
-assert (DT' === DT' #in# PerType) as HX1.
-eapply PER_Transitive with DT.
-symmetry; auto.
-auto.
-
-assert (Delta ||- t : T #aeq# dt' #in# HX1) as HX2.
-eapply RelTerm_ClosedUnderPer.
-eauto.
-eapply H.
-eauto.
-
-assert (PER PT) as HX3 by eauto.
-
-eapply RelTerm_ClosedUnderPer with (PT := PT).
-eauto.
-eauto.
-eauto.
-Qed.
-
-Lemma RelTerm_ClosedUnderPer_right: forall Delta t T DT DT' DT'' dt dt' PT
-  (HDT1 : DT === DT' #in# PerType) (HDT2: DT === DT'' #in# PerType),
-  dt === dt' #in# PT -> Interp DT PT ->
-  Delta ||- t : T #aeq# dt #in# HDT1 ->
-  Delta ||- t : T #aeq# dt' #in# HDT2
-.
-Proof.
-intros.
-
-assert (DT' === DT'' #in# PerType) as HX1.
-apply PER_Transitive with DT.
-symmetry; auto.
-auto.
-
-assert (Delta ||- t : T #aeq# dt #in# HX1 ) as HX2.
-eapply RelTerm_ClosedUnderPer with (PT := PT).
-eauto.
-eauto.
-eauto.
-
-
-assert (DT'' === DT #in# PerType ) as HX3.
-symmetry; auto.
-
-assert (Delta ||- t : T #aeq# dt #in#  HX3 ) as HX4.
-eapply RelTerm_ClosedUnderPer with (PT := PT).
-eauto.
-eauto.
-eauto.
-
-eapply RelTerm_ClosedUnderPer_sym with (PT := PT).
-eauto.
-eauto.
-eauto.
-Qed.
-
-(******************************************************************************
- * Helper
- *)
-
-
-Lemma F_tp_subst: forall Psi F j i a,
-  Psi |-- TmSb F (Sext (Sups (j + i)) a) ->
-  Psi |-- TmSb F (Sext (Sups (j + i)) a) === TmSb (TmSb F (Sext (Sseq (Sups i) Sup) TmVar)) (Sext (Sups j) a)
-.
-Proof.
-
-intros.
-
-clear_inversion H.
-clear_inversion H3.
-
-assert (Psi |-- [Sups (j + i)] === [Sseq (Sups i) (Sups j)] : Delta0) as HS1.
-apply Sups_tails; auto.
-
-assert (Psi |-- [Sseq (Sups i) (Sups j)] : Delta0) as HS2.
-eauto.
-
-assert (Psi |-- TmSb A (Sups (j + i))) as HS3.
-eauto.
-
-assert (Psi |-- TmSb A (Sups (j + i)) === TmSb (TmSb A (Sups i)) (Sups j)) as HS4.
-rewrite plus_comm.
-eapply Sups_tp_plus_eq.
-rewrite plus_comm.
-auto.
-
-assert (Psi |-- a : TmSb (TmSb A (Sups i)) (Sups j)) as HS5.
-eapply CONV.
-eauto.
-eauto.
-
-clear_inversion HS2.
-
-assert ( Gamma__1,, TmSb A (Sups i) |--  [Sext (Sseq (Sups i) Sup) TmVar] : Delta0,, A) as HS6.
-apply SEXT; auto.
-eauto.
-eapply CONV.
-eauto.
-eapply EQ_TP_SBSEQ.
-eauto.
-eauto.
-eauto.
-
-assert ( Psi |--  [Sext (Sups j) a] : Gamma__1,, TmSb A (Sups i) ) as HS7.
-eapply SEXT; eauto.
-
-eapply EQ_TP_SYM.
-eapply EQ_TP_TRANS.
-eapply EQ_TP_SBSEQ; eauto.
-eapply EQ_TP_CONG_SB; [ | eauto ].
-
-eapply EQ_SB_TRANS.
-eapply EQ_SB_SEXT; eauto.
-
-eapply EQ_SB_CONG_SEXT; auto.
-
-eapply EQ_SB_TRANS.
-eapply EQ_SB_COMM; eauto.
-
-eapply EQ_SB_TRANS.
-eapply EQ_SB_CONG_SSEQ.
-eapply EQ_SB_SUP; eauto.
-eauto.
-
-eapply EQ_SB_SYM.
-apply Sups_tails.
-eauto.
-
-eapply EQ_CONV.
-eapply EQ_SBVAR; eauto.
-
-(**)
-
-eapply EQ_TP_SYM.
-eapply EQ_TP_TRANS.
-eapply EQ_TP_CONG_SB; [ |  eauto ].
-eapply EQ_SB_TRANS.
-eapply EQ_SB_COMM; eauto.
-eapply EQ_SB_CONG_SSEQ.
-eapply EQ_SB_SUP; eauto.
-eauto.
-
-eapply EQ_TP_SYM.
-eapply EQ_TP_TRANS.
-eapply EQ_TP_SBSEQ; eauto.
-eauto.
-
-(*
- *   TmSb F (Sext (Sups (j + i)) a)
- *
- *   by Sups_tails
- * = TmSb F (Sext (Sseq (Sups j) (Sups i)) a)  
- *
- *   TmSb (TmSb F (Sext (Sseq (Sups i) Sup) TmVar)) (Sext (Sups j) a)
- *
- *   by Sups def
- * = TmSb (TmSb F (Sext (Sups (S i)) TmVar)) (Sext (Sups j) a)
- *
- *   by EQ_TP_SBSEQ
- * = TmSb F (Sseq (Sext (Sups (S i)) TmVar)) (Sext (Sups j) a)
- *
- *   by EQ_TP_CONG_SB and EQ_SB_SEXT
- * = TmSb F (Sext (Sseq (Sups (S i) (Sext (Sups j) a))) (TmSb TmVar (Sext (Sups j) a)))
- *
- * = TmSb F (Sext (Sseq (Sups i) (Sups j)) a)
- *
- * = TmSb F (Sext (Sups (i + j)) a)
- *
- * = TmSb F (Sext (Sups (j + i)) a)
- *)
-Qed.
-
-
-Lemma Inversion_FUN_E_ : forall Gamma N M T,
-  Gamma |-- TmApp M N : T ->
-  exists A F, Gamma |-- M : TmFun A F /\ Gamma |-- T === TmSb F (Ssing N) /\ Gamma |-- N : A
-.
-Proof.
-intros.
-
-remember (TmApp M N) as X1.
-generalize dependent M.
-generalize dependent N.
-
-induction H; intros; try solve [ clear_inversion HeqX1 ].
-clear_inversion HeqX1.
-
-exists A.
-exists B.
-split; auto.
-eauto.
-
-(**)
-
-subst.
-destruct (IHWtTm _ _ eq_refl) as [A' [F' [HH1 [HH2 HH3]]]].
-exists A' F'.
-split; auto.
-eauto.
-Qed.
-
-Lemma F_subst: forall Psi t F j i a,
-  Psi |-- TmApp (TmSb t (Sups (j + i))) a : TmSb F (Sext (Sups (j + i)) a) ->
-
-  Psi |-- TmApp (TmSb t (Sups (j + i))) a ===
-    TmApp (TmSb (TmSb t (Sups i)) (Sups j)) a : TmSb F (Sext (Sups (j + i)) a)
-.
-Proof.
-
-intros.
-
-edestruct Inversion_FUN_E_ as [A' [F' [HH1 [HH2 HH3]]]].
-eauto.
-
-eapply EQ_CONV.
-eapply EQ_CONG_FUN_E.
-rewrite plus_comm.
-eapply Sups_plus_eq.
-rewrite plus_comm.
-eauto.
-eauto.
-
-apply EQ_TP_SYM.
-auto.
-Qed.
-
-
-(******************************************************************************
- * Lifting
- *)
-
-Theorem RelLifting: forall Gamma T DT DT' (HDT : DT === DT' #in# PerType),
-  forall Delta i, CxtShift Delta i Gamma ->
-    (Gamma ||- T #in# HDT -> Delta ||- TmSb T (Sups i) #in# HDT) /\
-    (forall t dt, Gamma ||- t : T #aeq# dt #in# HDT -> Delta ||- TmSb t (Sups i) : TmSb T (Sups i) #aeq# dt #in# HDT)
-.
-Proof.
-intros until HDT.
-generalize dependent Gamma.
-generalize dependent T.
-induction HDT using PerType_dind; intros.
-
-(* Dnat 1 *)
-simpl in *.
-
-assert (Gamma |-- T === TmNat -> Delta |-- TmSb T (Sups i) === TmNat).
-intros.
-eapply EQ_TP_TRANS.
-eapply EQ_TP_CONG_SB.
-eapply EQ_SB_REFL.
-red in H. eauto.
-eauto.
-eapply EQ_TP_SB_NAT.
-eauto.
-
-split; auto.
-
-(* Dnat 2 *)
-
-simpl in *.
-program_simpl.
-split; auto.
-split; auto.
-intros.
-edestruct (H3 Delta0).
-eauto.
-program_simpl.
-exists x.
-split ;auto.
-eapply EQ_TRANS.
-eapply EQ_SYM.
-apply Sups_plus_eq.
-rewrite plus_comm.
-eauto.
-rewrite plus_comm.
-auto.
-
-(* Dunit 1 *)
-
-simpl in *.
-
-assert (Gamma |-- T === TmUnit -> Delta |-- TmSb T (Sups i) === TmUnit).
-intros.
-eapply EQ_TP_TRANS.
-eapply EQ_TP_CONG_SB.
-eapply EQ_SB_REFL.
-red in H. eauto.
-eauto.
-eapply EQ_TP_SB_UNIT.
-eauto.
-split; auto.
-
-(* Dunit 2 *)
-
-simpl in *.
-program_simpl.
-split; auto.
-split; auto.
-intros.
-edestruct (H3 Delta0).
-eauto.
-program_simpl.
-exists x.
-split ;auto.
-eapply EQ_TRANS.
-eapply EQ_SYM.
-apply Sups_plus_eq.
-rewrite plus_comm.
-eauto.
-rewrite plus_comm.
-auto.
-
-(* Dfun 1 *)
- 
-renamer.
-rename i into HDA.
-rename i2 into i.
-rename e into eDB.
-rename e0 into eDB'.
-rename i1 into HREC.
-rename H into IHF.
-rename IHHDT into IHA.
-rename i0 into HPDA.
-rename H0 into HCxtShift.
-
-split.
-intros.
-simpl in *.
-destruct H as [A [F [HS1 [HS2 HS3]]]].
-exists (TmSb A (Sups i)) (TmSb F (Sext (Sseq (Sups i) Sup) TmVar)).
-split.
-
-assert (Gamma |-- TmFun A F) by eauto.
-clear_inversion H.
-eauto.
-
-split.
-
-(**)
-
-specialize (IHA A Gamma Delta i HCxtShift).
-destruct IHA as [IHA_Type IHA_Term].
-auto.
-
-(**)
-
-intros Psi j a da DB DB' PA HPA Hda Happ Happ' HCxtShift' HP.
-specialize (HS3 Psi (j + i) a da DB DB').
-specialize (HS3 PA HPA Hda Happ Happ').
-
-
-specialize (CxtShift_comp); intro HCxtShift''.
-specialize (HCxtShift'' Gamma Delta i Psi j HCxtShift HCxtShift').
-specialize (HS3 HCxtShift'').
-
-
-assert ( Psi |-- a : TmSb (TmSb A (Sups i)) (Sups j) ) as HP1.
-eapply RelTerm_implies_WtTm.
-eauto.
-
-assert ( Psi |-- TmSb (TmSb A (Sups i)) (Sups j) ) as HP2.
-eauto.
-
-assert ( Psi ||- a : TmSb A (Sups (j + i)) #aeq# da #in# HDA ) as HP3.
-eapply RelTerm_ClosedForConversion.
-eauto.
-apply EQ_TP_SYM.
-rewrite plus_comm.
-apply Sups_tp_plus_eq'.
-eauto.
-eauto.
-apply EQ_REFL.
-auto.
-
-specialize (HS3 HP3).
-eapply RelType_ClosedForConversion.
-eauto.
-
-apply F_tp_subst.
-eapply RelType_implies_WfTp.
-eauto.
-
-(* Dfun 2 *)
-
-intros.
-simpl in *.
-destruct H as [HS1 [A [F [PT [HS2 [HS3 [HS4 [HS5 HS6]]]]]]]].
-
-repeat (split; auto).
-eauto.
-
-(**)
-
-exists (TmSb A (Sups i)) (TmSb F (Sext (Sseq (Sups i) Sup) TmVar)).
-exists PT.
-repeat (split; auto).
-
-assert (Gamma |-- TmFun A F) by eauto.
-clear_inversion H.
-eauto.
-
-(**)
-
-specialize (IHA A Gamma Delta i HCxtShift).
-destruct IHA as [IHA_Type IHA_Term].
-auto.
-
-(**)
-
-intros Psi j a da DB DB' PA HPA Hda Happ Happ' HCxtShift' HP.
-specialize (HS6 Psi (j + i) a da DB DB').
-specialize (HS6 PA HPA Hda Happ Happ').
-
-specialize (CxtShift_comp); intro HCxtShift''.
-specialize (HCxtShift'' Gamma Delta i Psi j HCxtShift HCxtShift').
-specialize (HS6 HCxtShift'').
-
-assert ( Psi |-- a : TmSb (TmSb A (Sups i)) (Sups j) ) as HP1.
-eapply RelTerm_implies_WtTm.
-eauto.
-
-assert ( Psi |-- TmSb (TmSb A (Sups i)) (Sups j) ) as HP2.
-eauto.
-
-assert ( Psi ||- a : TmSb A (Sups (j + i)) #aeq# da #in# HDA ) as HP3.
-eapply RelTerm_ClosedForConversion.
-eauto.
-apply EQ_TP_SYM.
-rewrite plus_comm.
-apply Sups_tp_plus_eq'.
-eauto.
-eauto.
-apply EQ_REFL.
-auto.
-
-specialize (HS6 HP3).
-
-destruct HS6 as [dy HS6].
-exists dy.
-destruct HS6 as [HS7 HS8].
-split; auto.
-
-eapply RelTerm_ClosedForConversion.
-eauto.
-
-apply F_tp_subst.
-eapply RelType_implies_WfTp.
-eauto.
-eauto.
-
-eapply F_subst.
-eapply RelTerm_implies_WtTm.
-eauto.
-
-(* Dempty 1 *)
-
-simpl in *.
-
-assert (Gamma |-- T === TmEmpty -> Delta |-- TmSb T (Sups i) === TmEmpty).
-intros.
-eapply EQ_TP_TRANS.
-eapply EQ_TP_CONG_SB.
-eapply EQ_SB_REFL.
-red in H. eauto.
-eauto.
-eapply EQ_TP_SB_EMPTY.
-eauto.
-split; auto.
-
-(* Dempty 2 *)
-
-simpl in *.
-program_simpl.
-split; auto.
-split; auto.
-intros.
-edestruct (H3 Delta0).
-eauto.
-program_simpl.
-exists x.
-split ;auto.
-eapply EQ_TRANS.
-eapply EQ_SYM.
-apply Sups_plus_eq.
-rewrite plus_comm.
-eauto.
-rewrite plus_comm.
-auto.
-
-Qed.
-
-(******************************************************************************
- * Unpacking lifting.
- *)
-
-Fact RelTypeLifting: forall Gamma T DT DT' (HDT : DT === DT' #in# PerType),
-  forall Delta i, CxtShift Delta i Gamma ->
-    Gamma ||- T #in# HDT -> Delta ||- TmSb T (Sups i) #in# HDT
-.
-Proof.
-intros.
-edestruct RelLifting; eauto.
-Qed.
-
-Fact RelTermLifting: forall Gamma T DT DT' (HDT : DT === DT' #in# PerType) t dt,
-  forall Delta i, CxtShift Delta i Gamma ->
-    Gamma ||- t : T #aeq# dt #in# HDT -> Delta ||- TmSb t (Sups i) : TmSb T (Sups i) #aeq# dt #in# HDT
-.
-Proof.
-intros.
-edestruct RelLifting; eauto.
-Qed.
-
-Fact Sups1_tpeq: forall Gamma A T,
-  Gamma,,A |-- TmSb T (Sups 1) ->
-  Gamma,,A |-- TmSb T (Sups 1) === TmSb T Sup
-.
-Proof.
-intros.
-assert (Gamma,,A |--) by eauto.
-clear_inversion H0.
-simpl in *.
-eapply EQ_TP_CONG_SB.
-eapply EQ_SB_SIDL. eauto.
-eapply EQ_TP_REFL.
-clear_inversion H.
-assert (Gamma,, A |-- [Sup] : Delta).
-eapply WtSb_SIDL; auto.
-clear_inversion H.
-auto.
-Qed.
-
-Fact Sups1_wt: forall Gamma A T,
-  Gamma |-- T ->
-  Gamma |-- A ->
-  Gamma,,A |-- TmSb T (Sups 1)
-.
-Proof.
-intros; simpl.
-eapply SB_F; auto.
-eapply SSEQ; eauto.
-auto.
-Qed.
-
-(******************************************************************************
- *)
-
-Corollary RelTypeLift1: forall Gamma A T DT DT' (HDT : DT === DT' #in# PerType),
-    Gamma ||- T #in# HDT -> Gamma |-- A -> Gamma,,A ||- TmSb T Sup #in# HDT
-.
-Proof.
-intros.
-remember (Gamma,,A) as Delta.
-eapply RelType_ClosedForConversion with (T := TmSb T (Sseq Sid Sup)).
-fold (Sups 1).
-eapply RelTypeLifting.
-red; subst; simpl; eauto.
-auto.
-subst; apply Sups1_tpeq.
-apply Sups1_wt.
-eapply RelType_implies_WfTp.
-eauto.
-eauto.
-Qed.
-
-(******************************************************************************
- *)
-
-Corollary RelTermLift1: forall Gamma A T DT DT' (HDT : DT === DT' #in# PerType) t dt,
-    Gamma ||- t : T #aeq# dt #in# HDT -> Gamma |-- A -> Gamma,,A ||- TmSb t Sup : TmSb T Sup #aeq# dt #in# HDT
-.
-Proof.
-intros.
-remember (Gamma,,A) as Delta.
-eapply RelTerm_ClosedForConversion with (T := TmSb T (Sseq Sid Sup)) (t := TmSb t (Sseq Sid Sup)); fold (Sups 1).
-eapply RelTypeLifting.
-red; subst; simpl; eauto.
-eapply RelTerm_implies_RelType; eauto.
-subst; apply Sups1_tpeq; auto.
-apply Sups1_wt; auto.
-eapply RelType_implies_WfTp; auto.
-eapply RelTerm_implies_RelType; eauto.
-(**)
-eapply RelTermLifting.
-subst; red; simpl; eauto.
-auto.
-(**)
-subst; simpl.
-eapply EQ_CONG_SB.
-eauto.
-eapply EQ_REFL.
-eapply RelTerm_implies_WtTm; auto.
-eauto.
-Qed.
-
-(******************************************************************************
- * Each
- *)
-
-
-Lemma TmVar_Sups_tmVar: forall i Delta  Gamma A,
-  CxtShift Delta i (Gamma,,A) ->
-  Delta |-- TmSb TmVar (Sups i) === tmVar i : TmSb (TmSb A Sup) (Sups i)
-.
-Proof.
-induction i; intros.
-
-clear_inversion H.
-simpl.
-clear_inversion H0.
-apply EQ_SBID.
-eapply CONV.
-eauto.
-eapply EQ_TP_SYM.
-eapply EQ_TP_SBID.
-eauto.
-
-(**)
-
-clear_inversion H.
-clear_inversion H3.
-rename A0 into B.
-simpl.
-
-specialize (IHi Gamma__1 Gamma A H5).
-eapply EQ_CONV.
- 
-eapply EQ_TRANS.
-eapply EQ_SYM.
-eapply EQ_SBSEQ.
-
-eauto.
-eauto.
-eauto.
-eapply EQ_CONG_SB.
-eauto.
-apply IHi.
-
-eapply EQ_TP_SBSEQ.
-eauto.
-eauto.
-eauto.
-Qed.
-
-(******************************************************************************
- *)
-
-
-Lemma TmVar_Sups_tmVar': forall i Delta  Gamma A,
-  CxtShift Delta i (Gamma,,A) ->
-  Delta |-- TmSb TmVar (Sups i) === tmVar i : TmSb (TmSb A (Sups 1)) (Sups i)
-.
-Proof.
-intros.
-simpl in *.
-
-assert (Gamma,,A |--).
-eauto.
-clear_inversion H0.
-
-eapply EQ_CONV.
-eapply TmVar_Sups_tmVar.
-eauto.
-eapply EQ_TP_SYM.
-eapply EQ_TP_CONG_SB.
-eauto.
-eapply EQ_TP_CONG_SB.
-eapply EQ_SB_SIDL.
-apply SUP.
-eauto.
-eauto.
-Qed.
-
-(******************************************************************************
- * Reification1
- *)
-
-Theorem RelReify1: forall Gamma T DT DT' (HDT : DT === DT' #in# PerType),
-  Gamma ||- T #in# HDT ->
-    (exists A, RbNf (length Gamma) (DdownN DT) A /\ Gamma |-- T === A
-    ) /\
-
-    (forall t dt, Gamma ||- t : T #aeq# dt #in# HDT ->
-      (exists v, RbNf (length Gamma) (Ddown DT dt) v /\ Gamma |-- t === v : T)
-    ) /\
-
-    (forall t k, k === k #in# PerNe ->
-      (forall Delta i, CxtShift Delta i Gamma -> exists tv,
-        RbNe (length Delta) k tv /\
-        Delta |-- TmSb t (Sups i) === tv : TmSb T (Sups i))
-      ->
-      Gamma ||- t : T #aeq# (Dup DT k) #in# HDT
-    )
-.
-Proof.
-do 5 intro.
-generalize dependent T.
-generalize dependent Gamma.
-induction HDT using PerType_dind; split; try split; intros.
-
-(*Dnat a) *)
-
-exists TmNat; auto.
-
-(*Dnat b) *)
-
-simpl in H0.
-decompose record H0.
-specialize (H4 Gamma 0).
-destruct H4; try red; eauto.
-exists x. simpl in *.
-decompose record H2.
-split; auto.
-eapply EQ_TRANS.
-eapply EQ_SYM.
-eapply EQ_SBID; eauto.
-eapply EQ_CONV; eauto.
-auto.
-
-(*Dnat c) *)
-
-simpl; repeat split; auto.
-intros.
-edestruct H1.
-eauto.
-program_simpl.
-exists x.
-split; auto.
-unfold Ddown; unfold Dup; simpl.
-apply reifyNf_ne; auto.
-simpl in H.
-eapply EQ_CONV.
-apply H4.
-eapply EQ_TP_TRANS.
-eapply EQ_TP_CONG_SB.
-eapply EQ_SB_REFL.
-red in H2. eauto.
-eauto.
-eapply EQ_TP_SB_NAT.
-eauto.
-
-(*Dunit a) *)
-
-exists TmUnit; auto.
-
-(*Dunit b) *)
-
-simpl in H0.
-decompose record H0.
-specialize (H4 Gamma 0).
-destruct H4; try red; eauto.
-exists x. simpl in *.
-decompose record H2.
-split; auto.
-eapply EQ_TRANS.
-eapply EQ_SYM.
-eapply EQ_SBID; eauto.
-eapply EQ_CONV; eauto.
-
-(*Dunit c) *)
-
-simpl; repeat split; auto.
-intros.
-
-exists Tm1.
-split; auto.
-unfold Ddown; unfold Dup; simpl; eauto.
-apply EQ_Unit_Eta.
-
-edestruct H1.
-eauto.
-program_simpl.
-simpl in H.
-eapply CONV.
-eauto.
-eapply EQ_TP_TRANS.
-eapply EQ_TP_CONG_SB.
-eapply EQ_SB_REFL.
-red in H2. eauto.
-eauto.
-eapply EQ_TP_SB_UNIT.
-eauto.
-
-(*Dfun a) *)
-
-renamer; intros.
-rename i into HDA.
-rename i1 into HREC.
-rename i0 into HPDA.
-rename e0 into e'.
-
-simpl in H0.
-destruct H0 as [A [F [HS1 [HS2 HS3]]]].