---

Step * 1 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 : 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])
BY
{ (EqTypeHD (-2) THENA Auto) }

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 ∈ pertype(λx,y. ((x ∈ T) ∧ (y ∈ T) ∧ E[x;y]))
14. y ∈ T
15. a ∈ T
16. E[y;a]
17. 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  :  Base
6.  a1  :  Base
7.  a  =  a1
8.  a  \mmember{}  T
9.  a1  \mmember{}  T
10.  E[a;a1]
11.  b  :  Base
12.  y  :  Base
13.  y  =  a
14.  y  \mleq{}  b
\mvdash{}  a  =  b


By

---

Latex:
(EqTypeHD  (-2)  THENA  Auto)

---

Home Index