Step * of Lemma interval-rev_wf

No Annotations
āˆ€[Gamma:jāŠ¢]. āˆ€[r:{Gamma āŠ¢ _:š•€}].  (1-(r) āˆˆ {Gamma āŠ¢ _:š•€})
BY
(Auto
   THEN MemTypeCD
   THEN Auto
   THEN RepUR ``interval-rev`` 0
   THEN Auto
   THEN (RWO "cubical-term-at-morph<THENA Auto)) }

1
1. Gamma CubicalSet{j}
2. {Gamma āŠ¢ _:š•€}
3. fset(ā„•)
4. fset(ā„•)
5. J āŸ¶ I
6. Gamma(I)
āŠ¢ (Ā¬(r(a)) f) = Ā¬((r(a) f)) āˆˆ š•€(f(a))


Latex:


Latex:
No  Annotations
\mforall{}[Gamma:j\mvdash{}].  \mforall{}[r:\{Gamma  \mvdash{}  \_:\mBbbI{}\}].    (1-(r)  \mmember{}  \{Gamma  \mvdash{}  \_:\mBbbI{}\})


By


Latex:
(Auto
  THEN  MemTypeCD
  THEN  Auto
  THEN  RepUR  ``interval-rev``  0
  THEN  Auto
  THEN  (RWO  "cubical-term-at-morph<"  0  THENA  Auto))




Home Index