Step
*
of Lemma
compU_wf1
No Annotations
∀[G:j⊢]. (compU() ∈ composition-function{j:l, i':l}(G; c𝕌))
BY
{ ((Auto THEN Unfold `compU` 0)
   THEN Unfold `composition-function` 0
   THEN RepeatFor 3 ((MemCD THENA Auto))
   THEN (RWW "csm-cubical-universe" 0 THENA Auto)
   THEN ThinVar `s'
   THEN ThinVar `G'
   THEN RenameVar `G' 1
   THEN BLemma `compU-wf-lemma1`
   THEN Auto) }
Latex:
Latex:
No  Annotations
\mforall{}[G:j\mvdash{}].  (compU()  \mmember{}  composition-function\{j:l,  i':l\}(G;  c\mBbbU{}))
By
Latex:
((Auto  THEN  Unfold  `compU`  0)
  THEN  Unfold  `composition-function`  0
  THEN  RepeatFor  3  ((MemCD  THENA  Auto))
  THEN  (RWW  "csm-cubical-universe"  0  THENA  Auto)
  THEN  ThinVar  `s'
  THEN  ThinVar  `G'
  THEN  RenameVar  `G'  1
  THEN  BLemma  `compU-wf-lemma1`
  THEN  Auto)
Home
Index