---

Step * of Lemma setmem-set-add

∀a,b,x:coSet{i:l}.  ((x ∈ a + b) ⇐⇒ (x ∈ a) ∨ (x ∈ b))
BY
{ (Intros
   THEN (coSetD 2 THEN D 2)
   THEN (coSetD 1 THEN D 1)
   THEN Auto
   THEN All SetMemDef
   THEN All (Fold `mk-coset`)
   THEN (All (RWO "setmem-mk-coset") THENA Auto)) }

1
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))

2
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. seteq(x;a1 t)) ∨ (∃t:T. seteq(x;b1 t))
⊢ ∃t:T1 + T. seteq(x;case t of inl(t) => a1 t | inr(s) => b1 s)

---

Latex:

---

Latex:
\mforall{}a,b,x:coSet\{i:l\}.    ((x  \mmember{}  a  +  b)  \mLeftarrow{}{}\mRightarrow{}  (x  \mmember{}  a)  \mvee{}  (x  \mmember{}  b))


By

---

Latex:
(Intros
  THEN  (coSetD  2  THEN  D  2)
  THEN  (coSetD  1  THEN  D  1)
  THEN  Auto
  THEN  All  SetMemDef
  THEN  All  (Fold  `mk-coset`)
  THEN  (All  (RWO  "setmem-mk-coset")  THENA  Auto))

---

Home Index