---

Step * 1 of Lemma quotient-mono


1. T : Type
2. mono(T)
3. E : T ⟶ T ⟶ ℙ
4. EquivRel(T;x,y.E[x;y])
5. a : x,y:T//E[x;y]
6. b : Base
7. is-above(x,y:T//E[x;y];a;b)
⊢ a = b ∈ (x,y:T//E[x;y])
BY
{ (DVar `a' THEN RepeatFor 2 (D -1)) }

1
1. T : Type
2. mono(T)
3. E : T ⟶ T ⟶ ℙ
4. EquivRel(T;x,y.E[x;y])
5. a : Base
6. a1 : Base
7. a = a1 ∈ pertype(λx,y. ((x ∈ T) ∧ (y ∈ T) ∧ E[x;y]))
8. a ∈ T
9. a1 ∈ T
10. E[a;a1]
11. b : Base
12. y : Base
13. y = a ∈ (x,y:T//E[x;y])
14. y ≤ b
⊢ a = b ∈ (x,y:T//E[x;y])

---

Latex:

---

Latex:

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


By

---

Latex:
(DVar  `a'  THEN  RepeatFor  2  (D  -1))

---

Home Index