---

Step * of Lemma bl-rev-exists-sq

∀[T:Type]. ∀[L:T List]. ∀[P:{x:T| (x ∈ L)}  ⟶ 𝔹].  ((∃x∈rev(L).P[x])_b ~ (∃x∈L.P[x])_b)
BY
{ xxx(InductionOnList
      THEN Unfolds ``bl-exists bl-rev-exists`` 0
      THEN Reduce 0
      THEN Try (Folds ``bl-exists bl-rev-exists`` 0)
      THEN (D 0 THENA Auto)
      THEN Try (Trivial))xxx }

1
1. T : Type
2. u : T
3. v : T List
4. ∀[P:{x:T| (x ∈ v)}  ⟶ 𝔹]. ((∃x∈rev(v).P[x])_b ~ (∃x∈v.P[x])_b)
5. P : {x:T| (x ∈ [u / v])}  ⟶ 𝔹
⊢ case (∃x∈rev(v).P[x])_b of inl(x) => tt | inr(x) => P[u] ~ P[u] ∨b(∃x∈v.P[x])_b

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[L:T  List].  \mforall{}[P:\{x:T|  (x  \mmember{}  L)\}    {}\mrightarrow{}  \mBbbB{}].    ((\mexists{}x\mmember{}rev(L).P[x])\_b  \msim{}  (\mexists{}x\mmember{}L.P[x])\_b)


By

---

Latex:
xxx(InductionOnList
        THEN  Unfolds  ``bl-exists  bl-rev-exists``  0
        THEN  Reduce  0
        THEN  Try  (Folds  ``bl-exists  bl-rev-exists``  0)
        THEN  (D  0  THENA  Auto)
        THEN  Try  (Trivial))xxx

---

Home Index