---

Step * 1 of Lemma list-cardinality-le


1. [T] : Type
2. L : T List@i
3. ∀x:T. (x ∈ L)@i
4. b : T@i
⊢ ∃a:ℕ||L||. (L[a] = b ∈ T)
BY
{ (((InstHyp [⌜b⌝] (-2))⋅ THENA Auto) THEN (Unfold `l_member` (-1)) THEN (ParallelOp (-1)) THEN ExRepD THEN Auto') }

---

Latex:

---

Latex:

1.  [T]  :  Type
2.  L  :  T  List@i
3.  \mforall{}x:T.  (x  \mmember{}  L)@i
4.  b  :  T@i
\mvdash{}  \mexists{}a:\mBbbN{}||L||.  (L[a]  =  b)


By

---

Latex:
(((InstHyp  [\mkleeneopen{}b\mkleeneclose{}]  (-2))\mcdot{}  THENA  Auto)
  THEN  (Unfold  `l\_member`  (-1))
  THEN  (ParallelOp  (-1))
  THEN  ExRepD
  THEN  Auto')

---

Home Index