---

Step * 1 of Lemma bl-rev-exists-sq


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
BY
{ xxx((RWO "-2" 0 THENA Auto)
      THEN (AutoBoolCase ⌜(∃x∈v.P[x])_b⌝⋅ THENA Auto)
      THEN ((AutoBoolCase ⌜P[u]⌝⋅ THENA Auto) THEN (RepUR ``bfalse btrue`` 0 THEN Auto)⋅)⋅)xxx }

---

Latex:

---

Latex:

1.  T  :  Type
2.  u  :  T
3.  v  :  T  List
4.  \mforall{}[P:\{x:T|  (x  \mmember{}  v)\}    {}\mrightarrow{}  \mBbbB{}].  ((\mexists{}x\mmember{}rev(v).P[x])\_b  \msim{}  (\mexists{}x\mmember{}v.P[x])\_b)
5.  P  :  \{x:T|  (x  \mmember{}  [u  /  v])\}    {}\mrightarrow{}  \mBbbB{}
\mvdash{}  case  (\mexists{}x\mmember{}rev(v).P[x])\_b  of  inl(x)  =>  tt  |  inr(x)  =>  P[u]  \msim{}  P[u]  \mvee{}\msubb{}(\mexists{}x\mmember{}v.P[x])\_b


By

---

Latex:
xxx((RWO  "-2"  0  THENA  Auto)
        THEN  (AutoBoolCase  \mkleeneopen{}(\mexists{}x\mmember{}v.P[x])\_b\mkleeneclose{}\mcdot{}  THENA  Auto)
        THEN  ((AutoBoolCase  \mkleeneopen{}P[u]\mkleeneclose{}\mcdot{}  THENA  Auto)  THEN  (RepUR  ``bfalse  btrue``  0  THEN  Auto)\mcdot{})\mcdot{})xxx

---

Home Index