---

Step * 1 2 1 1 1 of Lemma equipollent-distinct-representatives


1. A : Type
2. E : A ⟶ A ⟶ ℙ
3. EquivRel(A;x,y.E[x;y])
4. L : A List
5. (∀a,b∈L.  ¬E[a;b])
6. ∀a:A. (∃b∈L. E[a;b])
7. f : A ⟶ ℕ||L||
8. ∀a,b:A.  ((f a) = (f b) ∈ ℕ||L|| ⇐⇒ E[a;b])
9. ∀i:ℕ||L||. ∃a:A. ((f a) = i ∈ ℕ||L||)
10. f ∈ (x,y:A//E[x;y]) ⟶ ℕ||L||
11. a1 : x,y:A//E[x;y]
12. a2 : x,y:A//E[x;y]
13. (f a1) = (f a2) ∈ ℕ||L||
⊢ a1 = a2 ∈ (x,y:A//E[x;y])
BY
{ ((Dquotient2 (-3) THENA (Auto THEN Try (UseTrans y⋅)))
   THEN (Dquotient2 (-2) THENA (Auto THEN Try (UseTrans y⋅)))
   THEN EqTypeCD
   THEN Auto) }

---

Latex:

---

Latex:

1.  A  :  Type
2.  E  :  A  {}\mrightarrow{}  A  {}\mrightarrow{}  \mBbbP{}
3.  EquivRel(A;x,y.E[x;y])
4.  L  :  A  List
5.  (\mforall{}a,b\mmember{}L.    \mneg{}E[a;b])
6.  \mforall{}a:A.  (\mexists{}b\mmember{}L.  E[a;b])
7.  f  :  A  {}\mrightarrow{}  \mBbbN{}||L||
8.  \mforall{}a,b:A.    ((f  a)  =  (f  b)  \mLeftarrow{}{}\mRightarrow{}  E[a;b])
9.  \mforall{}i:\mBbbN{}||L||.  \mexists{}a:A.  ((f  a)  =  i)
10.  f  \mmember{}  (x,y:A//E[x;y])  {}\mrightarrow{}  \mBbbN{}||L||
11.  a1  :  x,y:A//E[x;y]
12.  a2  :  x,y:A//E[x;y]
13.  (f  a1)  =  (f  a2)
\mvdash{}  a1  =  a2


By

---

Latex:
((Dquotient2  (-3)  THENA  (Auto  THEN  Try  (UseTrans  y\mcdot{})))
  THEN  (Dquotient2  (-2)  THENA  (Auto  THEN  Try  (UseTrans  y\mcdot{})))
  THEN  EqTypeCD
  THEN  Auto)

---

Home Index