---

Step * 1 1 of Lemma pi-system-example_wf


1. P : pi_term()
2. l : Id List@i
⊢ apply-alist(NatDeq;ten-locs{$a,$b,$c,$d,$e,$f,$g,$h,$i,$j,$k}();||l|| + 4) ∈ Id?
BY
{ ((InstLemma `apply-alist_wf` [⌈ℕ⌉]⋅ THENA Auto) THEN BHyp -1  THEN Auto) }

1
.....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

---

Latex:

---

Latex:

1.  P  :  pi\_term()
2.  l  :  Id  List@i
\mvdash{}  apply-alist(NatDeq;ten-locs\{\$a,\$b,\$c,\$d,\$e,\$f,\$g,\$h,\$i,\$j,\$k\}();||l||  +  4)  \mmember{}  Id?


By

---

Latex:
((InstLemma  `apply-alist\_wf`  [\mkleeneopen{}\mBbbN{}\mkleeneclose{}]\mcdot{}  THENA  Auto)  THEN  BHyp  -1    THEN  Auto)

---

Home Index