Step * of Lemma closed-cubical-type-cumulativity

No Annotations
* ⊢ _} ⊆* ⊢_}
BY
((D THENA Auto) THEN -1 THEN -2 THEN Reduce -1 THEN -1 THEN MemTypeCD THEN Reduce THEN Auto) }


Latex:


Latex:
No  Annotations
\{  *  \mvdash{}  \_\}  \msubseteq{}r  \{  *  \mvdash{}'  \_\}


By


Latex:
((D  0  THENA  Auto)
  THEN  D  -1
  THEN  D  -2
  THEN  Reduce  -1
  THEN  D  -1
  THEN  MemTypeCD
  THEN  Reduce  0
  THEN  Auto)




Home Index