---

Step * 2 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. 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)
BY
{ (((D -1 THEN ExRepD) THENL [D 0 With ⌜inl t⌝ ; D 0 With ⌜inr t ⌝ ]) THEN Reduce 0 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.  (\mexists{}t:T1.  seteq(x;a1  t))  \mvee{}  (\mexists{}t:T.  seteq(x;b1  t))
\mvdash{}  \mexists{}t:T1  +  T.  seteq(x;case  t  of  inl(t)  =>  a1  t  |  inr(s)  =>  b1  s)


By

---

Latex:
(((D  -1  THEN  ExRepD)  THENL  [D  0  With  \mkleeneopen{}inl  t\mkleeneclose{}  ;  D  0  With  \mkleeneopen{}inr  t  \mkleeneclose{}  ])  THEN  Reduce  0  THEN  Auto)

---

Home Index