---

Step * 1 1 1 1 1 1 of Lemma coSet-equality2


1. x : coSet{i:l}
2. y : coSet{i:l}
3. ∀T:𝕌'. ((((a:Type × (a ⟶ T)) ⊆r T) ∧ (coSet{i:l} ⊆r T)) ⇒ (x = y ∈ T) ⇒ (x = y ∈ (a:Type × (a ⟶ T))))
4. T : 𝕌'
5. (a:Type × (a ⟶ T)) ⊆r T
6. coSet{i:l} ⊆r T
7. ∀x@0,y@0:coSet{i:l}.  (((x@0 = x ∈ coSet{i:l}) ∧ (y@0 = y ∈ coSet{i:l})) ⇒ (x@0 = y@0 ∈ T))
8. a : coSet{i:l}
9. b : coSet{i:l}
10. a = x ∈ coSet{i:l}
11. b = y ∈ coSet{i:l}
12. x = y ∈ (a:Type × (a ⟶ T))
⊢ a = b ∈ (a:Type × (a ⟶ T))
BY
{ ((Assert x = a ∈ (a:Type × (a ⟶ T)) BY
          (SubsumeC ⌜a:Type × (a ⟶ coSet{i:l})⌝⋅ THEN Auto))
   THEN (Assert y = b ∈ (a:Type × (a ⟶ T)) BY
               (SubsumeC ⌜a:Type × (a ⟶ coSet{i:l})⌝⋅ THEN Auto))
   THEN Eq) }

---

Latex:

---

Latex:

1.  x  :  coSet\{i:l\}
2.  y  :  coSet\{i:l\}
3.  \mforall{}T:\mBbbU{}'.  ((((a:Type  \mtimes{}  (a  {}\mrightarrow{}  T))  \msubseteq{}r  T)  \mwedge{}  (coSet\{i:l\}  \msubseteq{}r  T))  {}\mRightarrow{}  (x  =  y)  {}\mRightarrow{}  (x  =  y))
4.  T  :  \mBbbU{}'
5.  (a:Type  \mtimes{}  (a  {}\mrightarrow{}  T))  \msubseteq{}r  T
6.  coSet\{i:l\}  \msubseteq{}r  T
7.  \mforall{}x@0,y@0:coSet\{i:l\}.    (((x@0  =  x)  \mwedge{}  (y@0  =  y))  {}\mRightarrow{}  (x@0  =  y@0))
8.  a  :  coSet\{i:l\}
9.  b  :  coSet\{i:l\}
10.  a  =  x
11.  b  =  y
12.  x  =  y
\mvdash{}  a  =  b


By

---

Latex:
((Assert  x  =  a  BY
                (SubsumeC  \mkleeneopen{}a:Type  \mtimes{}  (a  {}\mrightarrow{}  coSet\{i:l\})\mkleeneclose{}\mcdot{}  THEN  Auto))
  THEN  (Assert  y  =  b  BY
                          (SubsumeC  \mkleeneopen{}a:Type  \mtimes{}  (a  {}\mrightarrow{}  coSet\{i:l\})\mkleeneclose{}\mcdot{}  THEN  Auto))
  THEN  Eq)

---

Home Index