Commits

Paweł Wieczorek committed d7b738e

Working on the _Absurd case

Comments (0)

Files changed (1)

Nbe/Model/LogRelSb.v

 renamer.
 clear_dups.
 
+
+(**)
+
 assert ( Delta0 |-- [Sseq SB (Sups i)] : Gamma ) as HXX2.
 eauto.
 
 eauto.
 
 
+assert (Delta0 |-- a :  TmSb TmEmpty (Sups i)) as HXX4.
+eapply RelTerm_implies_WtTm.
+eauto.
+
+assert (Delta0 |-- a :  TmEmpty) as HXX5.
+eapply CONV.
+eauto.
+eapply EQ_TP_SB_EMPTY.
+eauto.
+
+assert (Delta0 |--  [Sext (Sups i) a]: Delta,,TmEmpty) as HXX7.
+eapply SEXT.
+eauto.
+eauto.
+eauto.
+
+
+assert (Delta0 |--  TmSb (TmSb A (Sseq SB Sup)) (Sext (Sups i) a) === TmSb A (Sseq SB (Sups i))) as HXX6.
+eapply EQ_TP_TRANS.
+eapply EQ_TP_SBSEQ.
+eauto.
+eauto.
+eauto.
+
+eapply EQ_TP_CONG_SB.
+eapply EQ_SB_TRANS.
+eapply EQ_SB_COMM.
+eauto.
+eauto.
+eauto.
+
+eapply EQ_SB_CONG_SSEQ.
+eapply EQ_SB_SUP.
+eauto.
+eapply EMPTY_F.
+eauto.
+eauto.
+eapply EQ_SB_REFL.
+eauto.
+eauto.
+
+(**)
+
+assert ( Delta0 ||- TmSb (TmSb A (Sseq SB Sup)) (Sext (Sups i) a)
+   #in# HREC (Dup Dempty e) (Dup Dempty e) DA_envs0 DB' PerEmpty HPA Hda Happ
+          Happ') as HZZ2.
+
+eapply RelType_ClosedForConversion.
+eauto.
+eauto.
+
 specialize (H0 _ _ _ HXX3).
 specialize (H0 _ _ (HREC (Dup Dempty e) (Dup Dempty e) DA_envs0 DB' PerEmpty HPA Hda Happ
           Happ')).
 eauto.
 destruct H8 as [RelTerm_Reify_ RelTerm_Back_ ].
 rename H4 into RelType_Reify_.
-
-(**)
 eapply RelTerm_Back_.
-eauto.
-
-assert (Delta0 |-- a :  TmSb TmEmpty (Sups i)) as HXX4.
-eapply RelTerm_implies_WtTm.
-eauto.
-
-assert (Delta0 |-- a :  TmEmpty) as HXX5.
-eapply CONV.
-eauto.
-eapply EQ_TP_SB_EMPTY.
-eauto.
-
-assert (Delta0 |--  [Sext (Sups i) a]: Delta,,TmEmpty) as HXX7.
-eapply SEXT.
-eauto.
-eauto.
-eauto.
-
-
-assert (Delta0 |--  TmSb (TmSb A (Sseq SB Sup)) (Sext (Sups i) a) === TmSb A (Sseq SB (Sups i))) as HXX6.
-eapply EQ_TP_TRANS.
-eapply EQ_TP_SBSEQ.
-eauto.
-eauto.
-eauto.
-
-eapply EQ_TP_CONG_SB.
-eapply EQ_SB_TRANS.
-eapply EQ_SB_COMM.
-eauto.
-eauto.
-eauto.
-
-eapply EQ_SB_CONG_SSEQ.
-eapply EQ_SB_SUP.
-eauto.
-eapply EMPTY_F.
-eauto.
-eauto.
-eapply EQ_SB_REFL.
-eauto.
-eauto.
-
-(**)
-
-specialize (H0 _ _ _ HXX3).
-specialize (H0 _ _ (HREC (Dup Dempty e) (Dup Dempty e) DA_envs0 DB' PerEmpty HPA Hda Happ
-          Happ')).
-specialize (H0 H15).
-
-
-
-eapply RelType_ClosedForConversion.
-eauto.
-eauto.
+
 
 (****)
 renamer.
-assert (DdownN DA_envs === DdownN DA_envs #in# PerNf) as HXX4.
-
-assert (Gamma |= A) as HXX2.
+assert (DdownN DA_envs === DdownN DA_envs #in# PerNf) as HXXX4.
+
+assert (Gamma |= A) as HXXX2.
 eapply Valid_for_WfTp.
 eauto.
 
 
-clear_inversion HXX2.
-assert ([envs] === [envs] #in# Gamma) as HXX3.
+clear_inversion HXXX2.
+assert ([envs] === [envs] #in# Gamma) as HXXX3.
 eapply RelSb_valenv.
 eauto.
 
-specialize (H8 _ _ HXX3).
+specialize (H8 _ _ HXXX3).
 destruct H8 as [DA_ [ _DA [_HDA [HDA_ HDA]]]].
 
 elim_deters.
 eapply ReifyTp_Characterization.
 eauto.
 eauto.
-clear_inversion HXX4.
-
+clear_inversion HXXX4.
 
 (**)
 constructor 1.
 
 intros.
 renamer.
-assert (DdownN DA_envs === DdownN DA_envs #in# PerNf) as HXX4.
-
-assert (Gamma |= A) as HXX2.
+assert (DdownN DA_envs === DdownN DA_envs #in# PerNf) as HXXX4.
+
+assert (Gamma |= A) as HXXX2.
 eapply Valid_for_WfTp.
 eauto.
 
 
-clear_inversion HXX2.
-assert ([envs] === [envs] #in# Gamma) as HXX3.
+clear_inversion HXXX2.
+assert ([envs] === [envs] #in# Gamma) as HXXX3.
 eapply RelSb_valenv.
 eauto.
 
-specialize (H10 _ _ HXX3).
+specialize (H10 _ _ HXXX3).
 destruct H10 as [DA_ [ _DA [_HDA [HDA_ HDA]]]].
 
 elim_deters.
 eapply ReifyTp_Characterization.
 eauto.
 eauto.
-clear_inversion HXX4.
+clear_inversion HXXX4.
 inversion H5; subst.
 
 edestruct H10 as [ne [Hne1 Hne2]].