---

Step * of Lemma name-case_wf

∀[T:Type]. ∀[A:i:Id ─→ {k:Knd| ↑hasloc(k;i)}  ─→ T]. ∀[B:Id ─→ Id ─→ T]. ∀[n:MaName].
  (name-case(n;i,k.A[i;k];j,x.B[j;x]) ∈ T)
BY
{ (Auto THEN Unfold `name-case` 0 THEN D -1 THEN Reduce 0 THEN Auto) }

---

Latex:


\mforall{}[T:Type].  \mforall{}[A:i:Id  {}\mrightarrow{}  \{k:Knd|  \muparrow{}hasloc(k;i)\}    {}\mrightarrow{}  T].  \mforall{}[B:Id  {}\mrightarrow{}  Id  {}\mrightarrow{}  T].  \mforall{}[n:MaName].
    (name-case(n;i,k.A[i;k];j,x.B[j;x])  \mmember{}  T)


By

(Auto  THEN  Unfold  `name-case`  0  THEN  D  -1  THEN  Reduce  0  THEN  Auto)

---

Home Index