---

Step * 1 of Lemma prop-truncation-quot


1. T : Type
2. ⇃(⇃(T))
3. a : ⇃(T)
4. b : ⇃(T)
⊢ a = b ∈ ⇃(T)
BY
{ (newQuotientElim1 (-2)⋅ THEN Try (CpltAuto)) }

1
1. T : Type
2. ⇃(⇃(T))
3. T ∈ Type
4. ∀x,y:T.  (True ∈ Type)
5. ∀x:T. True
6. b : ⇃(T)
7. x : T
8. y : T
9. True
10. ⇃(T) = ⇃(T) ∈ Type
⊢ x = b ∈ ⇃(T)

---

Latex:

---

Latex:

1.  T  :  Type
2.  \00D9(\00D9(T))
3.  a  :  \00D9(T)
4.  b  :  \00D9(T)
\mvdash{}  a  =  b


By

---

Latex:
(newQuotientElim1  (-2)\mcdot{}  THEN  Try  (CpltAuto))

---

Home Index