---

Step * 1 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 ∈ 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])
BY
{ (Assert y = b ∈ T BY
         (BackThruSomeHyp' THEN D 0 With ⌜y⌝  THEN 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
18. y = b ∈ T
⊢ 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  \mmember{}  T
15.  a  \mmember{}  T
16.  E[y;a]
17.  y  \mleq{}  b
\mvdash{}  a  =  b


By

---

Latex:
(Assert  y  =  b  BY
              (BackThruSomeHyp'  THEN  D  0  With  \mkleeneopen{}y\mkleeneclose{}    THEN  Auto))

---

Home Index