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<" 0 THENA Auto)) }
1
1. Gamma : CubicalSet{j}
2. r : {Gamma ā¢ _:š}
3. I : fset(ā)
4. J : fset(ā)
5. f : J ā¶ I
6. a : Gamma(I)
ā¢ (Ā¬(r(a)) a f) = Ā¬((r(a) 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