---

Step * of Lemma rev-type-line-0

No Annotations
∀[Gamma:j⊢]. ∀[A:{Gamma.𝕀 ⊢ _}].  (((A)-)[0(𝕀)] ~ (A)[1(𝕀)])
BY
{ (Intros
   THEN UseWitness ⌜Ax⌝⋅
   THEN MemCD
   THEN RepUR ``rev-type-line interval-rev`` 0
   THEN CsmUnfolding
   THEN RWO "dma-neg-dM0" 0
   THEN Auto) }

---

Latex:

---

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


By

---

Latex:
(Intros
  THEN  UseWitness  \mkleeneopen{}Ax\mkleeneclose{}\mcdot{}
  THEN  MemCD
  THEN  RepUR  ``rev-type-line  interval-rev``  0
  THEN  CsmUnfolding
  THEN  RWO  "dma-neg-dM0"  0
  THEN  Auto)

---

Home Index