---

Step * 1 of Lemma subtype_quotient


1. T : Type
2. E : T ⟶ T ⟶ ℙ
3. EquivRel(T;x,y.E[x;y])
4. [a] : Base
5. [b] : Base
6. [c] : a = b ∈ T
⊢ a ∈ x,y:T//E[x;y]
BY
{ (At ⌜Type⌝ PerMemCD⋅ THEN Reduce 0 THEN Try (Fold `quotient` 0) THEN Auto) }

---

Latex:

---

Latex:

1.  T  :  Type
2.  E  :  T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}
3.  EquivRel(T;x,y.E[x;y])
4.  [a]  :  Base
5.  [b]  :  Base
6.  [c]  :  a  =  b
\mvdash{}  a  \mmember{}  x,y:T//E[x;y]


By

---

Latex:
(At  \mkleeneopen{}Type\mkleeneclose{}  PerMemCD\mcdot{}  THEN  Reduce  0  THEN  Try  (Fold  `quotient`  0)  THEN  Auto)

---

Home Index