---

Step * of Lemma deq-member-firstn

∀[A:Type]. ∀[eq:EqDecider(A)]. ∀[L:A List]. ∀[n:ℕ+].
  ∀[x:A]. (x ∈b firstn(n;L) ~ x ∈b firstn(n - 1;L) ∨b(eqof(eq) x L[n - 1])) supposing n - 1 < ||L||
BY
{ ((Auto THEN BLemma `iff_imp_equal_bool`)
   THEN Auto
   THEN All (RW assert_pushdownC)
   THEN Auto
   THEN Try ((Unfold `eqof` 0 THEN Auto))) }

1
1. A : Type
2. eq : EqDecider(A)
3. L : A List
4. n : ℕ+
5. n - 1 < ||L||
6. x : A
7. (x ∈ firstn(n;L))
⊢ (x ∈ firstn(n - 1;L)) ∨ (x = L[n - 1] ∈ A)

2
1. A : Type
2. eq : EqDecider(A)
3. L : A List
4. n : ℕ+
5. n - 1 < ||L||
6. x : A
7. (x ∈ firstn(n - 1;L)) ∨ (x = L[n - 1] ∈ A)
⊢ (x ∈ firstn(n;L))

---

Latex:

---

Latex:
\mforall{}[A:Type].  \mforall{}[eq:EqDecider(A)].  \mforall{}[L:A  List].  \mforall{}[n:\mBbbN{}\msupplus{}].
    \mforall{}[x:A].  (x  \mmember{}\msubb{}  firstn(n;L)  \msim{}  x  \mmember{}\msubb{}  firstn(n  -  1;L)  \mvee{}\msubb{}(eqof(eq)  x  L[n  -  1]))  supposing  n  -  1  <  ||L||


By

---

Latex:
((Auto  THEN  BLemma  `iff\_imp\_equal\_bool`)
  THEN  Auto
  THEN  All  (RW  assert\_pushdownC)
  THEN  Auto
  THEN  Try  ((Unfold  `eqof`  0  THEN  Auto)))

---

Home Index