---

Step * 1 of Lemma setmem-set-add


1. T1 : Type
2. a1 : T1 ⟶ coSet{i:l}
3. T : Type
4. b1 : T ⟶ coSet{i:l}
5. x : coSet{i:l}@i'
6. t : T1 + T@i
7. seteq(x;case t of inl(t) => a1 t | inr(s) => b1 s)
⊢ (∃t:T1. seteq(x;a1 t)) ∨ (∃t:T. seteq(x;b1 t))
BY
{ (DProdsAndUnions THEN All Reduce THEN Auto) }

---

Latex:

---

Latex:

1.  T1  :  Type
2.  a1  :  T1  {}\mrightarrow{}  coSet\{i:l\}
3.  T  :  Type
4.  b1  :  T  {}\mrightarrow{}  coSet\{i:l\}
5.  x  :  coSet\{i:l\}@i'
6.  t  :  T1  +  T@i
7.  seteq(x;case  t  of  inl(t)  =>  a1  t  |  inr(s)  =>  b1  s)
\mvdash{}  (\mexists{}t:T1.  seteq(x;a1  t))  \mvee{}  (\mexists{}t:T.  seteq(x;b1  t))


By

---

Latex:
(DProdsAndUnions  THEN  All  Reduce  THEN  Auto)

---

Home Index