---

Step * of Lemma quotient-top-union-top-not-subtype

¬(⇃(Top + Top) ⊆r (Top + Top))
BY
{ ((D 0 THENA Auto)
   THEN (Assert (inl ⋅) = (inr ⋅ ) ∈ (Top + Top) BY
               (SubsumeC ⌜⇃(Top + Top)⌝⋅ THEN Auto THEN EqTypeCD THEN Auto))
   ) }

1
1. ⇃(Top + Top) ⊆r (Top + Top)
2. (inl ⋅) = (inr ⋅ ) ∈ (Top + Top)
⊢ False

---

Latex:

---

Latex:
\mneg{}(\00D9(Top  +  Top)  \msubseteq{}r  (Top  +  Top))


By

---

Latex:
((D  0  THENA  Auto)
  THEN  (Assert  (inl  \mcdot{})  =  (inr  \mcdot{}  )  BY
                          (SubsumeC  \mkleeneopen{}\00D9(Top  +  Top)\mkleeneclose{}\mcdot{}  THEN  Auto  THEN  EqTypeCD  THEN  Auto))
  )

---

Home Index