---

Step * 1 1 1 of Lemma pi-system-example_wf

.....wf..... 
1. P : pi_term()
2. l : Id List@i
3. ∀[eq:EqDecider(ℕ)]. ∀[x:ℕ]. ∀[V:Type]. ∀[L:(ℕ × V) List].  (apply-alist(eq;L;x) ∈ V?)
⊢ ten-locs{$a,$b,$c,$d,$e,$f,$g,$h,$i,$j,$k}() ∈ (ℕ × Id) List
BY
{ (Unfold `ten-locs` 0 THEN Auto) }

---

Latex:

---

Latex:
.....wf..... 
1.  P  :  pi\_term()
2.  l  :  Id  List@i
3.  \mforall{}[eq:EqDecider(\mBbbN{})].  \mforall{}[x:\mBbbN{}].  \mforall{}[V:Type].  \mforall{}[L:(\mBbbN{}  \mtimes{}  V)  List].    (apply-alist(eq;L;x)  \mmember{}  V?)
\mvdash{}  ten-locs\{\$a,\$b,\$c,\$d,\$e,\$f,\$g,\$h,\$i,\$j,\$k\}()  \mmember{}  (\mBbbN{}  \mtimes{}  Id)  List


By

---

Latex:
(Unfold  `ten-locs`  0  THEN  Auto)

---

Home Index