Commits

Paweł Wieczorek committed bebfd81

universe almost works

  • Participants
  • Parent commits 8dbf899
  • Branches universe_dirty_subset

Comments (0)

Files changed (2)

 doc/.*\.aux
 doc/.*\.backup
 Makefile.bak
+html

Nbe/LogicalRelations/FundamentalTheorem/WtTm_UnivTypeJudgements.v

 Require Import Nbe.LogicalRelations.Lift.
 
 
+
+
 Require Import Nbe.LogicalRelations.FundamentalTheorem.WtTm_GeneralJudgements.
 Require Import Nbe.LogicalRelations.FundamentalTheorem.WfTp_GeneralJudgements.
 Require Import Nbe.LogicalRelations.FundamentalTheorem.WtSb_GeneralJudgements.
 
 rename Delta0 into Psi.
 
+assert (Psi ||- TmSb (TmSb A SB) (Sups i0) : TmSb (TmSb TmUniv SB) (Sups i0) #aeq# DA #in# HDuniv) as HX13.
+{
+eapply RelTermLifting; eauto.
+}
+
+