---

Step * of Lemma rev-type-line-1

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

---

Latex:

---

Latex:
No  Annotations
\mforall{}[Gamma:j\mvdash{}].  \mforall{}[A:\{Gamma.\mBbbI{}  \mvdash{}  \_\}].    (((A)-)[1(\mBbbI{})]  \msim{}  (A)[0(\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-dM1"  0
  THEN  Auto)

---

Home Index