---

Step * 1 of Lemma concat-lifting-loc-1-strict


1. f : Top
2. i : Top
⊢ f@ i {} ~ {}
BY
{ (RW (BasicSymbolicComputeC []) 0 THEN Auto) }

---

Latex:

---

Latex:

1.  f  :  Top
2.  i  :  Top
\mvdash{}  f@  i  \{\}  \msim{}  \{\}


By

---

Latex:
(RW  (BasicSymbolicComputeC  [])  0  THEN  Auto)

---

Home Index