---

Step * of Lemma kindcase-rcv

∀[k:Knd]. ∀[f,g:Top].  kindcase(k;a.f[a];l,t.g[l;t]) ~ g[lnk(k);tag(k)] supposing ¬↑islocal(k)
BY
{ ((D 0 THENA Auto) THEN KindCase 1 THEN Auto THEN (D (-1)) THEN Auto) }

---

Latex:


\mforall{}[k:Knd].  \mforall{}[f,g:Top].    kindcase(k;a.f[a];l,t.g[l;t])  \msim{}  g[lnk(k);tag(k)]  supposing  \mneg{}\muparrow{}islocal(k)


By

((D  0  THENA  Auto)  THEN  KindCase  1  THEN  Auto  THEN  (D  (-1))  THEN  Auto)

---

Home Index