---

Step * 1 1 of Lemma prop-truncation-quot


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)
BY
{ (newQuotientElim1 (-5)⋅ THEN Try (CpltAuto)) }

---

Latex:

---

Latex:

1.  T  :  Type
2.  \00D9(\00D9(T))
3.  T  \mmember{}  Type
4.  \mforall{}x,y:T.    (True  \mmember{}  Type)
5.  \mforall{}x:T.  True
6.  b  :  \00D9(T)
7.  x  :  T
8.  y  :  T
9.  True
10.  \00D9(T)  =  \00D9(T)
\mvdash{}  x  =  b


By

---

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

---

Home Index