---

Step * 1 1 of Lemma st-lookup_wf

.....subterm..... T:t
1:n
1. T : Id ─→ Type
2. K : ℕ
3. t2 : ℕ
4. t3 : ℕK ─→ (Atom1 × ℕ + Atom1 × data(T))
5. x : Atom1
⊢ λn.(t2 <z n ∨bK ≤z n ∨bfst((t3 n)) =a1 x) ∈ ℕ ─→ 𝔹
BY
{ ((MemCD THENA Auto) THEN AutoBoolCase K ≤z n⋅) }

---

Latex:


.....subterm.....  T:t
1:n
1.  T  :  Id  {}\mrightarrow{}  Type
2.  K  :  \mBbbN{}
3.  t2  :  \mBbbN{}
4.  t3  :  \mBbbN{}K  {}\mrightarrow{}  (Atom1  \mtimes{}  \mBbbN{}  +  Atom1  \mtimes{}  data(T))
5.  x  :  Atom1
\mvdash{}  \mlambda{}n.(t2  <z  n  \mvee{}\msubb{}K  \mleq{}z  n  \mvee{}\msubb{}fst((t3  n))  =a1  x)  \mmember{}  \mBbbN{}  {}\mrightarrow{}  \mBbbB{}


By

((MemCD  THENA  Auto)  THEN  AutoBoolCase  K  \mleq{}z  n\mcdot{})

---

Home Index