---

Step * 2 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]) = (b ∈ x,y:T//E[x;y]) ∈ Type
BY
{ (EqCD THEN Auto) }

1
.....subterm..... T:t
2:n
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 = b ∈ (x,y:T//E[x;y])

---

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])  =  (b  \mmember{}  x,y:T//E[x;y])


By

---

Latex:
(EqCD  THEN  Auto)

---

Home Index