---

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

∀[f,i:Top].  (f@ i {} ~ {})
BY
{ Auto }

1
1. f : Top
2. i : Top
⊢ f@ i {} ~ {}

---

Latex:

---

Latex:
\mforall{}[f,i:Top].    (f@  i  \{\}  \msim{}  \{\})


By

---

Latex:
Auto

---

Home Index